HomSeamFluxHalfPin

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

The test-class constant at the print's own Schauder provenance α = 1/2

Why this file exists

The printed test-class pin cgTestConstBase d (homS M) (7 homS M/8) p′ gauges the Step-4 dual pairing test at Hölder order α = s = |log γ|⁻¹. The order gap of the conversion is then α - s′ = s/8, PROPORTIONAL to s, so the radial kernel's geometric factor (1 - 3^{-(α-s′)p′})⁻¹ degenerates like (s p′)⁻¹, and the constant DIVERGES like |log γ|^{1/p′} (the machine-proved lower-bound chain). Since the pairing constant is linear in it, the envelope condition C_w ≤ C_w⁰ of HomSchauderUniform.spineClauseConst_le_abs is unsatisfiable at that pin.

The print does NOT gauge the test at order s. It derives the W^{s,∞} bound of the Step-4 test from C^{0,1/2} Schauder data, whose scale weight is the display's own 3^{m(1/2-s)}; the DATA leg of this tree already received that fixed-gap treatment (cgOverlapDataConst, taken at the gap 1/2 - 49/100, model-free by type), the TEST leg never did.

Re-pinning α:= 1/2 keeps the dual order s′ = 7s/8 where the pairing needs it and evaluates the geometric factor at the FIXED gap 1/2 - 7s/8 ≥ 9/32. cgTestConstBase_half_le below is the resulting bound: γ-free, s-free, d-and-p′-only.

What this file supplies

• recutKtestHalf — the re-pinned test-class constant, and recutKtestHalfBound its model-free majorant (cgTestConstBase_half_le + recutKtestHalf_le_bound);
• recutCwHalfFluxAt — the free-Ccg pairing constant of HomSeamFluxFreeCcg with that constant in the K_test slot;
• pairCwLegOf_le_of_bounds — the generic leg envelope: at sbase ≤ B and κ ≤ κ₀ the leg is bounded by an sbase-free and κ-free quantity;
• THE ENVELOPE LEMMA recutCwHalfFluxAt_le_envelope: recutCwHalfFluxAt … ≤ C_w⁰ at every M, at the explicit C_w⁰ = recutCwHalfEnvelope d hd1 Ccg Cgap Cen0 — a function of d, the printed exponent, C_gap and C_en⁰ alone. This is exactly the statement measured to be FALSE at the α = s pin;
• spineClauseConst_le_abs_half — the immediate consequence: the K_abs frame condition of the re-cut bundle closes BEFORE the model.

Cen0 stays a free slot throughout: whether the energy-slot constant supplied for it is itself model-uniform is a separate question, still open, and no claim about it is made here.

1. The conversion at the Schauder provenance α = 1/2

theorem Algsuperdiff.Section4.Provider.Homogenization.cgAnnulusRatio_half_eq (d : ℕ) (s t : ℝ) : Regularity.annulusRatio d (cgGagliardoBeta d (1 / 2) (7 * s / 8) t) = 3 ^ (-((1 / 2 - 7 * s / 8) * t))

The annulus ratio of the (1/2, 7s/8, t) conversion: the geometric ratio is 3^{-(1/2 - 7s/8)t}, whose order gap does NOT close with s.

theorem Algsuperdiff.Section4.Provider.Homogenization.cgRadialKernelConst_half_le (d : ℕ) {s t : ℝ} (hs : s ≤ 1 / 4) (ht : 0 < t) : Regularity.radialKernelConst d (cgGagliardoBeta d (1 / 2) (7 * s / 8) t) ≤ 3 ^ d * 2 ^ d / (1 - 3 ^ (-(t / 4)))

THE FIXED-GAP RADIAL CONSTANT. At α = 1/2 the radial-kernel constant of the (7s/8, t) conversion is bounded by the s-FREE quantity 3^d 2^d (1 - 3^{-t/4})⁻¹, for every base order s ≤ 1/4: the order gap is at least 1/4, so the geometric factor never degenerates. Contrast the radialKernelConst_pinned_ge, where the same constant at α = s grows like s⁻¹ = |log γ|.

theorem Algsuperdiff.Section4.Provider.Homogenization.cgTestConstBase_half_le (d : ℕ) {s t : ℝ} (hs : s ≤ 1 / 4) (ht : 0 < t) : cgTestConstBase d (1 / 2) (7 * s / 8) t ≤ ↑d * (1 + (3 ^ d * 2 ^ d / (1 - 3 ^ (-(t / 4)))) ^ t⁻¹)

THE γ-UNIFORM TEST-CLASS CONSTANT. At the Schauder provenance α = 1/2, for every base order s ≤ 1/4 and every dual exponent t > 0,

  cgTestConstBase d (1/2) (7s/8) t  ≤  d (1 + (3^d 2^d (1 - 3^{-t/4})⁻¹)^{1/t}),

with NO s — hence no γ — on the right.

2. The re-pinned test constant and its model-free majorant

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.recutKtestHalf (d : ℕ) (hd1 : 1 ≤ d) (M : Section3.ABKModel d) : ℝ

THE RE-PINNED TEST-CLASS CONSTANT. The printed test-class pin with the Hölder gauge moved from α = s to the print's own Schauder provenance α = 1/2; the dual order s′ = 7s/8 is UNCHANGED.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.recutKtestHalfBound (d : ℕ) (hd1 : 1 ≤ d) : ℝ

The model-free majorant of the re-pinned test-class constant: d and the printed conjugate exponent only.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.recutKtestHalf_nonneg (d : ℕ) (hd1 : 1 ≤ d) (M : Section3.ABKModel d) (hlog : 4 ≤ |Real.log M.gamma|) : 0 ≤ recutKtestHalf d hd1 M

theorem Algsuperdiff.Section4.Provider.Homogenization.recutKtestHalf_le_bound (d : ℕ) (hd1 : 1 ≤ d) (M : Section3.ABKModel d) (hlog : 4 ≤ |Real.log M.gamma|) : recutKtestHalf d hd1 M ≤ recutKtestHalfBound d hd1

THE TEST CONSTANT IS γ-UNIFORM AT THE RE-PIN. This is the machine fact the D2 re-cut rests on: the majorant names d and the printed exponent only.

theorem Algsuperdiff.Section4.Provider.Homogenization.recutKtestHalfBound_nonneg (d : ℕ) (hd1 : 1 ≤ d) : 0 ≤ recutKtestHalfBound d hd1

3. The generic leg envelope

theorem Algsuperdiff.Section4.Provider.Homogenization.pairCwLegOf_le_of_bounds (d : ℕ) {Ccg : ℝ} (p : HCPolySupport.FiniteLpExponent) (s2 : ↑HCPolySupport.FractionalOrder) {Cgap Cen0 sbase kappa theta B kappa0 : ℝ} (hCcg0 : 0 ≤ Ccg) (hCgap : 0 < Cgap) (hCen0 : 0 ≤ Cen0) (hsbase : 0 < sbase) (hkappa : 0 ≤ kappa) (hkle : kappa ≤ kappa0) (htheta : 0 < theta) (hB : sbase ≤ B) (hBs2 : theta * B < ↑s2) (hCdata0 : 0 ≤ cgOverlapDataConst d s2 p) (hs2gap : 5 < 10 * ↑s2 * Real.log 3) : pairCwLegOf d Ccg p s2 Cgap Cen0 sbase kappa theta ≤ kappa0 * Ccg * theta⁻¹ * Cen0 + kappa0 * Ccg * theta ^ (-(9 / 2)) * (↑s2 - theta * B)⁻¹ * cgOverlapDataConst d s2 p * homGapConstAt ↑s2 / Cgap

THE LEG ENVELOPE. pairCwLegOf is bounded by a quantity free of the base order sbase (only sbase ≤ B is used) and of the multiplier κ (only κ ≤ κ₀). Both degenerations live in the two factors bounded here: the (θ sbase)⁻¹ ⬝ sbase cancellation is EXACT, and the window factor (s₂ - θ sbase)⁻¹ is monotone in sbase.

4. The re-pinned pairing constant and THE ENVELOPE

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.recutCwHalfFluxAt (d : ℕ) (hd1 : 1 ≤ d) (M : Section3.ABKModel d) (Ccg Cgap Cen0 : ℝ) : ℝ

The free-Ccg pairing constant of HomSeamFluxFreeCcg at the re-pinned test constant.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.recutCwHalfEnvelope (d : ℕ) (hd1 : 1 ≤ d) (Ccg Cgap Cen0 : ℝ) : ℝ

THE MODEL-FREE PAIRING ENVELOPE, at the numeral pin p = 4d, s₂ = 49/100, B = 1/4 (the gate homS M ≤ 1/4). A function of d, the printed exponent, C_gap and C_en⁰ — no M, hence no γ.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.recutCwHalfFluxAt_le_envelope (d : ℕ) (hd1 : 1 ≤ d) (M : Section3.ABKModel d) {Ccg Cgap Cen0 : ℝ} (hCcg0 : 0 ≤ Ccg) (hCgap : 0 < Cgap) (hCen0 : 0 ≤ Cen0) (hlog : 4 ≤ |Real.log M.gamma|) : recutCwHalfFluxAt d hd1 M Ccg Cgap Cen0 ≤ recutCwHalfEnvelope d hd1 Ccg Cgap Cen0

THE ENVELOPE LEMMA.

The pairing constant of the re-cut lane, at the Schauder-provenance test pin, is bounded by a quantity that does not mention the model. This is the statement measured to be UNSATISFIABLE at the α = s pin (it grows like |log γ|^{1-1/(4d)}): the ONLY model-dependent factor of pairCwOf was the test constant, and at α = 1/2 it is bounded by recutKtestHalfBound.

theorem Algsuperdiff.Section4.Provider.Homogenization.recutCwHalfEnvelope_nonneg (d : ℕ) (hd1 : 1 ≤ d) {Ccg Cgap Cen0 : ℝ} (hCcg0 : 0 ≤ Ccg) (hCgap : 0 < Cgap) (hCen0 : 0 ≤ Cen0) : 0 ≤ recutCwHalfEnvelope d hd1 Ccg Cgap Cen0

The envelope is nonnegative on its own terms — no model is consulted.

theorem Algsuperdiff.Section4.Provider.Homogenization.spineClauseConst_le_abs_half (d : ℕ) (hd1 : 1 ≤ d) (M : Section3.ABKModel d) {Ccg Cgap Cen0 : ℝ} (hCcg0 : 0 ≤ Ccg) (hCgap : 0 < Cgap) (hCen0 : 0 ≤ Cen0) (hlog : 4 ≤ |Real.log M.gamma|) : spineClauseConst d (homS M) (recutExponent d hd1).exponent.toReal (recutCwHalfFluxAt d hd1 M Ccg Cgap Cen0) (stepFourSchauderConstU d) ≤ (2 * stepFourSchauderConstU d + 288 * ↑d ^ 2) * recutCwHalfEnvelope d hd1 Ccg Cgap Cen0

THE K_abs FRAME CONDITION, CLOSED BEFORE THE MODEL, AT THE RE-PIN.

HomSchauderUniform.spineClauseConst_le_abs fed by the envelope: the absorbed constant of the two clause displays is bounded by a quantity naming only d, the printed exponent, C_gap and C_en⁰.