Assembly

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

p.cg.ellipticity.bounds: the two-leg assembly and the constant normalization

Proposition p.cg.ellipticity.bounds (ABK26, statement) is a single ∃ C(d) carrying two displays under one constant: e.cg.ellip.lower and e.cg.ellip.upper. Its frozen Lean surface is Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds.

This module is the assembly layer directly below that frozen statement. It contains no analysis at all: it is the exact bookkeeping that lets the two displays be proved independently, each with its own constant, and then be combined into the frozen statement, and it is the exact bookkeeping that lets a consumer normalize the frozen constant.

What is proved here

• coarse_ellipticity_bounds_body_of_legs --- from the lower display at a constant Clow > 0 and the upper display at a constant Cup > 0, the frozen ∀-body at any common Ccg ≥ max Clow Cup.
• coarse_ellipticity_bounds_of_legs --- the lossless conditional assembly. From the two legs, each in its own ∃ C > 0 form, it derives the frozen statement verbatim, at Ccg = max Clow Cup. The proved frozen export now uses the exact application

  exact Algsuperdiff.Section3.Provider.CoarseEllipticity.coarse_ellipticity_bounds_of_legs
    d hlower hupper
  

  at the assembly layer, with hlower and hupper supplied by the proved production legs.

Why the constant may be increased (the direction of every slot)

• max (exp (C / sigma)) cstar⁻¹ ≤ E --- an hypothesis, and it is stronger at the larger constant (sigma > 0), so it implies the hypothesis at the smaller one.
• s ∈ Icc (gamma/2 + exp (-(C⁻¹E⁻²gamma⁻¹))) 1 --- an hypothesis, and its lower endpoint increases with C (because C⁻¹ decreases and E⁻²gamma⁻¹ ≥ 0), so the window at the larger constant is contained in the window at the smaller one.
• the deterministic lower profile lowerEllipticityProfile C gamma s q --- a conclusion slot, and it increases with C in each of the three branches (lowerEllipticityProfile_mono_const).
• the rare-lane scale exp (-(C⁻¹E⁻²gamma⁻¹)) --- a conclusion slot, and it increases with C.
• the upper deterministic shift C and its typical amplitude C cstar⁻¹ s gamma (2s-gamma)⁻³ --- conclusion slots, both increasing in C on the source window (cstar > 0, s > 0, gamma > 0, 2s - gamma > 0).

The two positivity facts 0 < s and 0 < 2 * s - gamma used above are theorems from the source window, not binders: the window's lower endpoint gamma/2 + exp(...) already exceeds gamma/2.

The proof-term slot of the observables

The frozen statement passes the positivity proof 0 < s to Observable.cutoffLowerEllipticityInv / Observable.cutoffUpperEllipticity as an explicit argument, built from hsWindow.1. A leg stated at Clow builds that argument from its window. The two terms are proofs of the same Prop and are therefore definitionally equal, so the observables literally coincide; no transport is needed and none is performed.

What is not claimed

This module itself does not prove or assign status to p.cg.ellipticity.bounds. What is delivered here is that the node factors through two independently typed leg statements and that the frozen constant can be normalized; this helper carries no node status.

References

• ABK26, p.cg.ellipticity.bounds, statement, proof; e.cg.ellip.lower, e.cg.ellip.upper.
• All three are already encoded in the frozen statement and in Algsuperdiff/Section3/Exponent.lean; this module changes none of them.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.coarse_ellipticity_bounds_body_of_legs (d : ℕ) {Clow Cup Ccg : ℝ} (hClow : 0 < Clow) (hCup : 0 < Cup) (hlowle : Clow ≤ Ccg) (huple : Cup ≤ Ccg) (hlow : ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Clow / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => Observable.cutoffLowerEllipticityInv M m L s ⋯ q omega * ↑(Annealed.sigmaBar M (m - 1))) (m - 1) (lowerEllipticityProfile Clow M.gamma s q) (Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))) (hup : ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Cup / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Cup⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), Probability.IsDeterministicShiftTwoTermOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffUpperEllipticity M m m s ⋯ q omega * (↑(Annealed.sigmaBar M (m - 1)))⁻¹) Cup (Cup * (Disorder.cstar M)⁻¹ * s * M.gamma * (2 * s - M.gamma)⁻¹ ^ 3) (Real.exp (-(Cup⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))) (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }) : Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Ccg / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => Observable.cutoffLowerEllipticityInv M m L s ⋯ q omega * ↑(Annealed.sigmaBar M (m - 1))) (m - 1) (lowerEllipticityProfile Ccg M.gamma s q) (Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) ∧ Probability.IsDeterministicShiftTwoTermOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffUpperEllipticity M m m s ⋯ q omega * (↑(Annealed.sigmaBar M (m - 1)))⁻¹) Ccg (Ccg * (Disorder.cstar M)⁻¹ * s * M.gamma * (2 * s - M.gamma)⁻¹ ^ 3) (Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

The two-leg assembly, on the ∀-body.

From the lower coarse-ellipticity display at a constant Clow and the upper one at a constant Cup, the frozen statement's ∀-body holds at any common constant Ccg dominating both. Every slot moves in the direction that makes this monotonicity, and only monotonicity; see the module docstring.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.coarse_ellipticity_bounds_of_legs (d : ℕ) (hlower : ∃ (Clow : ℝ), 0 < Clow ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Clow / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => Observable.cutoffLowerEllipticityInv M m L s ⋯ q omega * ↑(Annealed.sigmaBar M (m - 1))) (m - 1) (lowerEllipticityProfile Clow M.gamma s q) (Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))) (hupper : ∃ (Cup : ℝ), 0 < Cup ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Cup / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Cup⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), Probability.IsDeterministicShiftTwoTermOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffUpperEllipticity M m m s ⋯ q omega * (↑(Annealed.sigmaBar M (m - 1)))⁻¹) Cup (Cup * (Disorder.cstar M)⁻¹ * s * M.gamma * (2 * s - M.gamma)⁻¹ ^ 3) (Real.exp (-(Cup⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))) : ∃ (Ccg : ℝ), 0 < Ccg ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Ccg / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => Observable.cutoffLowerEllipticityInv M m L s ⋯ q omega * ↑(Annealed.sigmaBar M (m - 1))) (m - 1) (lowerEllipticityProfile Ccg M.gamma s q) (Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) ∧ Probability.IsDeterministicShiftTwoTermOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffUpperEllipticity M m m s ⋯ q omega * (↑(Annealed.sigmaBar M (m - 1)))⁻¹) Ccg (Ccg * (Disorder.cstar M)⁻¹ * s * M.gamma * (2 * s - M.gamma)⁻¹ ^ 3) (Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

Lossless conditional assembly for p.cg.ellipticity.bounds.

From the two printed displays, each supplied with its own dimension-only constant, the frozen statement verbatim, at the combined constant max Clow Cup. Both displays remain explicit A arguments of this helper. The concrete downstream theorems superposedFlux_coarse_ellipticity_lower_leg and superposedFlux_coarse_ellipticity_upper_leg supply the two arguments; this conditional helper itself carries no node status.