HomSeamStepOneDisplay

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Step 1's display at the re-pinned base s/8 and the ENLARGED Y

What this file supplies

HomSeamSpineBase.StepOneDisplayAt at

  sb = homSeamBase M hs = s/8,
  Y  = seamEnlargedY M m C_top Y₀
     = C_top · Y₀ · (1 + 𝓔sup_{1/8})(1 + 𝓔sup_{1/4}),

i.e. the sibling of Step 1's own display at the re-pinned base AND at the enlarged Y slot (HomSpineTopScale.stepTwoEnlargedY at the consumer pin t = 1/4). Two moves, one display.

The bookkeeping

The anchor is consumed through the exists_ethmB_seam_factor_moments at the boosted exponent

  q = max( 8p, 64 d |log γ| ),

and the five slots land at 4p, 4p, 2p (the three EthmB factors at the re-pinned base) and 8p, 8p (the two enlarged-Y factors). The Theorem-C edge Y₀ is used at 4p, one Hölder step above the 2p — this is the ×16 on the printed p-range, and it is absorbed into the produced constant, never into a hypothesis.

t⁻¹ = 4 is kept displayed: at the consumer pin t = 1/4 it is the constant 4, so the display stays at |log γ|².

The numeric collapse

HomStepOneDisplay.display_collapse is reused verbatim; the two seam moves contribute exactly one bounded scalar factor

  κ = 8 · C_top · (1 + 𝓔-budget)²  ≤  8 C_top (1 + 8 A D)²,

the 8 being the re-pinned base's own (s/8)⁻¹ = 8|log γ|. seam_display_collapse is that observation and nothing more.

1. The enlarged Y slot

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.seamEnlargedY {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (Ctop : ℝ) (Y0 : Section3.Cutoff.CutoffSample d → ENNReal) : Section3.Cutoff.CutoffSample d → ENNReal

THE ENLARGED Y SLOT, as one function.

C_top · Y₀ · stepTwoEnlargedY, with the enlargement at the consumer pin t = 1/4: the deterministic Step-2 constant, the Theorem-C minimal-scale factor, and the two honest error indices of the two-index Step-2 display.

Equations

• One or more equations did not get rendered due to their size.

2. The Hölder budget of the enlargement

theorem Algsuperdiff.Section4.Provider.Homogenization.seamEnlargedY_moment {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) {t : ℝ} (ht : 0 < t) (Y0 : Section3.Cutoff.CutoffSample d → ENNReal) (hY0m : AEMeasurable Y0 ↑(Section3.Cutoff.cutoffSampleLaw M)) {Ctop : ℝ} (hCtop : 0 ≤ Ctop) {p R4 R5 : ℝ} (hp : 1 ≤ p) (hR4 : 0 ≤ R4) (hR5 : 0 ≤ R5) (hY0 : ∫⁻ (w : Section3.Cutoff.CutoffSample d), Y0 w ^ (4 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal 2 ^ (4 * p)) (h4 : ∫⁻ (w : Section3.Cutoff.CutoffSample d), Support.fluxCorrectedTwoScaleErrorObservableSup M m m ⟨t / 2, ⋯⟩ w ^ (8 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal R4 ^ (8 * p)) (h5 : ∫⁻ (w : Section3.Cutoff.CutoffSample d), Support.fluxCorrectedTwoScaleErrorObservableSup M m m ⟨t, ht⟩ w ^ (8 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal R5 ^ (8 * p)) : ∫⁻ (w : Section3.Cutoff.CutoffSample d), (ENNReal.ofReal Ctop * (Y0 w * stepTwoEnlargedY M m ht w)) ^ (2 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (Ctop * (2 * ((1 + R4) * (1 + R5)))) ^ (2 * p)

THE ENLARGED-Y HÖLDER BUDGET.

The 2p-moment of C_top · (Y₀ · stepTwoEnlargedY) from the Theorem-C edge at 4p and the two new 𝓔-moments at 8p. This is the measured bookkeeping, executed.

3. The seam collapse constants

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homSeamSqrtLoss (d : ℕ) : ℝ

The √max loss of the re-pinned boosted exponent q = max(8p, 64 d |log γ|).

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homSeamSqrtLoss d = 3 + 8 * √↑d

theorem Algsuperdiff.Section4.Provider.Homogenization.homSeamSqrtLoss_nonneg (d : ℕ) : 0 ≤ homSeamSqrtLoss d

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homSeamCollapseConst (A : ℝ) (d : ℕ) : ℝ

The two display_collapse budgets, added.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Homogenization.homSeamCollapseConst_nonneg {A : ℝ} (hA : 0 ≤ A) (d : ℕ) : 0 ≤ homSeamCollapseConst A d

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homSeamKappa (A Ctop : ℝ) (d : ℕ) : ℝ

The seam enlargement's bounded scalar factor: the re-pinned base's own 8, the deterministic Step-2 constant, and the two (1 + 𝓔) budgets.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homSeamKappa A Ctop d = 8 * Ctop * (1 + 8 * A * Algsuperdiff.Section4.Provider.Homogenization.homSeamSqrtLoss d) ^ 2 + 1

theorem Algsuperdiff.Section4.Provider.Homogenization.one_le_homSeamKappa {A Ctop : ℝ} (hA : 0 ≤ A) (hCtop : 0 ≤ Ctop) (d : ℕ) : 1 ≤ homSeamKappa A Ctop d

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homSeamDisplayConst (A Ctop Cgate : ℝ) (d : ℕ) : ℝ

The produced constant of the seam display. The 8A summand is the q = 8p boost of the p-range, the 2 C_gate summand is the Theorem-C edge's own 4p reading, and the product is the collapse budget times the enlargement's scalar.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Homogenization.one_le_homSeamDisplayConst {A Ctop Cgate : ℝ} (hA : 0 ≤ A) (hCtop : 0 ≤ Ctop) (hCgate : 0 ≤ Cgate) (d : ℕ) : 1 ≤ homSeamDisplayConst A Ctop Cgate d

4. The seam collapse

5. Two range transfers

6. THE SEAM DISPLAY

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_ethmB_seam_moment_bound (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) {Ctop Cgate : ℝ} (hCtop : 0 ≤ Ctop) (hCgate : 0 < Cgate) : ∃ (gamma0 : ℝ) (C0 : ℝ), 0 < gamma0 ∧ 1 ≤ C0 ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (hs : 0 < homS M) (m : ℤ) (Y0 : Section3.Cutoff.CutoffSample d → ENNReal), AEMeasurable Y0 ↑(Section3.Cutoff.cutoffSampleLaw M) → (∀ (p : ℝ), 1 ≤ p → p ≤ Cgate⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (w : Section3.Cutoff.CutoffSample d), Y0 w ^ (2 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal 2 ^ (2 * p)) → ∀ (Cgap : ℝ), 0 ≤ Cgap → StepOneDisplayAt M Cgap (seamEnlargedY M m Ctop Y0) m (homSeamBase M hs) C0

STEP 1's DISPLAY AT THE RE-PINNED BASE AND THE ENLARGED Y.

HomSeamSpineBase.StepOneDisplayAt at sb = s/8 and Y = seamEnlargedY M m C_top Y₀, from the five re-pinned factor moments, the Theorem-C edge Y₀ read at 4p, and display_collapse.

Every hypothesis is either the anchor's own (inside exists_ethmB_seam_factor_moments) or the Theorem-C edge hY₀ at the gate constant C_gate; nothing else is assumed.