HomStepOneSeamAnchor

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

Theorem B, §4.5, Step 1 RE-PINNED: the anchor at the base

s/8 and at the two enlarged-Y indices

What this module is

The SIBLING of the anchor's Step-1 factor moments, at the two re-pins the §4.5 lane now carries:

• the BASE re-pin s ↦ s/8 of HomSeamRepin.homSeamBase (an INSTANTIATION of the HomStepEnvelope.ethmB, no new object): the two mesoscale 𝓔 factors move from s/2, s/4 to s/16, s/32;
• the Y-slot ENLARGEMENT of HomSpineTopScale.stepTwoEnlargedY (discharged at K_idx = 1 by HomSpineTopScale.stepTwoIndexBridge_of_representative): the printed minimal-scale slot Y = 3^{(1-α)X_m(α)} is multiplied by the two honest Step-2 indices (1 + 𝓔_{t/2,∞,2}(□_m))(1 + 𝓔_{t,∞,2}(□_m)). Those are two MORE 𝓔 factors for the print's own Step-1 Hölder budget (the bounds_mathcal_E_aL lemma moments), and they are produced here.

So the eighth anchor is applied FIVE times rather than three:

factor	anchor exponent s'	gap m − n	anchor bracket s'⁻¹ + √(m−n)
𝓔_{s'/2}(□_m, n), s' = s/8	s/16	k	≤ 18|log γ|
𝓔_{1/4}(□_m)	1/4	0	= 4
𝓔_{s'/4}(□_m, n), s' = s/8	s/32	k	≤ 34|log γ|
𝓔_{t/2}(□_m) (enlarged Y)	t/2	0	= 2 t⁻¹
𝓔_{t}(□_m) (enlarged Y)	t	0	= t⁻¹

with s = |log γ|⁻¹, k = ⌈10|log γ|⌉, n = m − k.

The three numerals, machine-measured

• the quartic γ-gauge 16 → 128. The anchor's lower s-endpoint C_A² √γ ≤ s' binds at the SMALLEST slot, which is now homQuarterOf (homSeamBase M hs) = s/32 instead of the s/4. Via absLog_mul_sqrt_le (|log γ|√γ ≤ 4 γ^{1/4}) the requirement is 32 · 4 · C_A² γ^{1/4} ≤ 1, i.e. γ^{1/4} ≤ (128 C_A²)⁻¹ — exactly eight times the (16 C_A²)⁻¹. This is homSeamGamma0 below.
• the q-range lower gate 8d|log γ| → 64 d |log γ|. The binding slot is again s/32: the anchor asks 2d (s/32)⁻¹ = 64 d |log γ| ≤ q, and the hypothesis hq_lo sits AT that equality. The scaling is therefore exactly ×8 off the 8 d |log γ|, matching the gauge's ×8. The 32 d |log γ| was understated by a factor two.
• the upper endpoint homConst C_A = 200 max(C_A, 1) is UNCHANGED. The tightest divisor of the q-upper endpoint moves 4 → 32, and the produced constant must dominate 3 · C_A · 34 = 102 C_A (the s/32 slot, with the IMPROVED 3-power, see below); both fit under 200 max(C_A,1), headroom 200/32 on the endpoint and 200/102 on the majorant.

The 3-power budget IMPROVES and is what keeps 200 sufficient: at the re-pinned base the anchor exponents are (1/2)(s/16)k ≤ 3/8 and (1/2)(s/32)k ≤ 3/16, so 3^{·} ≤ 3 (rpow_three_le_three) replaces the 3^{·} ≤ 27. With the 27 the s/32 slot would need 27 · 34 C_A = 918 C_A and 200 would NOT suffice.

The index bookkeeping of the enlarged Y (the honest binders)

The two new factors sit at gap 0 (n = m), so their 3-power is 3^0 = 1 and their bracket is exactly (t/2)⁻¹ = 2 t⁻¹ resp. t⁻¹. The anchor's own admissible range then forces exactly two binders on t, both DISPLAYED:

• t ≤ 1/4 — the anchor's s-range has the CLOSED right endpoint 1/4. This is a genuine NARROWING of the correction's t < 1/2; the consumer must choose its Step-2 Besov index at or below 1/4. Nothing else in the Step-2 chain resists: t ≤ 1/4 < 1/2 is strictly stronger than what needs.
• homS M / 8 ≤ t — i.e. t at or above the re-pinned base. This is what keeps BOTH new slots inside the single gate 64 d |log γ|: 2d (t/2)⁻¹ = 4 d t⁻¹ ≤ 32 d |log γ| and 2 d t⁻¹ ≤ 16 d |log γ|. It also supplies the anchor's lower s-endpoint for them, since C_A² √γ ≤ s/32 ≤ s/16 ≤ t/2. It is a vanishing constraint (s/8 ≤ 1/32 and s → 0 with γ), so any fixed positive Step-2 index satisfies it for small γ.

CORRECTION to this file brief: the gate moves to 64 d |log γ| because of the s/32 slot of the BASE re-pin, NOT because of the two new factors. The new factors are merely ACCOMMODATED by 64 d |log γ|, and only under homS M / 8 ≤ t.

t⁻¹ is kept VISIBLE in the two new majorants rather than absorbed into |log γ| (no silent absorption of a parameter-dependent quantity). At the consumer's natural choice t = 1/4 it is the constant 4, so the Step-1 display's |log γ|² is NOT degraded; had it been absorbed by t⁻¹ ≤ 8|log γ| the display would have had to carry |log γ|³.

1. The re-pinned γ-threshold

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.homSeamGamma0 (CA : ℝ) : ℝ

The γ-threshold of the RE-PINNED Step-1 factor bounds. Branch one is the anchor's lower s-endpoint at the SMALLEST slot s/32 (128 C_A² γ^{1/4} ≤ 1 in the quartic gauge — eight times the 16 of the anchor's own threshold), branch two is the anchor's own γ-gate, unchanged.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.homSeamGamma0 CA = min ((128 * max CA 1 ^ 2)⁻¹ ^ 4) ((max CA 1)⁻¹ ^ 10)

theorem Algsuperdiff.Section4.Provider.Homogenization.homSeamGamma0_pos (CA : ℝ) : 0 < homSeamGamma0 CA

2. 3^x ≤ 3: the improved exponent budget

theorem Algsuperdiff.Section4.Provider.Homogenization.rpow_three_le_three {x : ℝ} (hx : x ≤ 1) : Real.rpow 3 x ≤ 3

At the re-pinned base the anchor's 3-power exponents are below 1, so the 3^x ≤ 27 can be sharpened to 3^x ≤ 3. This is exactly the slack that keeps the produced constant at 200 max(C_A,1).

3. The majorant core, over abstract reals

4. The five re-pinned Step-1 factor moments

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_ethmB_seam_factor_moments (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 1 ≤ C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (hs : 0 < homS M) (m : ℤ) (t : ℝ) (ht : 0 < t), homS M / 8 ≤ t → t ≤ 1 / 4 → ∀ (q : ℝ), 64 * ↑d * |Real.log M.gamma| ≤ q → q ≤ C⁻¹ * M.gamma⁻¹ * homS M → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.fluxCorrectedTwoScaleErrorObservableSup M m (homN M m) (homHalf (homSeamBase M hs)) omega ^ q ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * |Real.log M.gamma| * √q * √M.gamma) ^ q ∧ ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.fluxCorrectedTwoScaleErrorObservableSup M m m homQuarter omega ^ q ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * √q * √M.gamma) ^ q ∧ ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.fluxCorrectedTwoScaleErrorObservableSup M m (homN M m) (homQuarterOf (homSeamBase M hs)) omega ^ q ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * |Real.log M.gamma| * √q * √M.gamma) ^ q ∧ ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.fluxCorrectedTwoScaleErrorObservableSup M m m ⟨t / 2, ⋯⟩ omega ^ q ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * t⁻¹ * √q * √M.gamma) ^ q ∧ ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.fluxCorrectedTwoScaleErrorObservableSup M m m ⟨t, ht⟩ omega ^ q ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * t⁻¹ * √q * √M.gamma) ^ q

THE RE-PINNED STEP-1 FACTOR MOMENTS.

The sibling of the anchor's Step-1 factor moments at the re-pinned base homSeamBase M hs = s/8 AND at the two enlarged-Y indices t/2, t of HomSpineTopScale.stepTwoEnlargedY. The bounds_mathcal_E_aL lemma is applied five times; every hypothesis below is either one of the anchor's own binders, discharged here, or one of the four displayed gates (homS M / 8 ≤ t, t ≤ 1/4, 64 d |log γ| ≤ q, q ≤ C⁻¹ γ⁻¹ s).

The t⁻¹ of the last two majorants is deliberately NOT absorbed into |log γ|; see the module docstring.