EllipticityBranchLow

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

The coarse-ellipticity branch of l.bad.event.lemma at n < m

BadEventLemmaCases.lean supplies a conditional local result for the coarse-ellipticity branch of ABK26's Lemma l.bad.event.lemma on the branch n >= m. This module supplies a conditional local result for the other branch, n < m:

lambda^{-1}_{1/8,2}(square_m; a_n)
  <= max_{z in 3^n Z^d cap square_m} lambda^{-1}_{1/8,2}(z + square_n; a_n) ,

then p.cg.ellipticity.bounds at each translate and l.maximums.Gamma.s.

The two corrections this branch runs under

• The printed max form is false at finite q. Definition (2.23) puts a sum of per-depth maxima on the left and a maximum of sums on the right, and the printed step fails by 3^{2(m-n)(d/q-s)}, unbounded in the separation. The consuming step is routed instead through the true q = infinity max form and exponent monotonicity, reading the coarse-graining input at a fixed t < s; the canonical instantiation is t = 1/16. This module consumes the proved gap-constant route (sharp only relative to the geometric profile) ErrorComparison.lambdaSq_eighth_inv_le_two_mul_max_descendants_sixteenth (lambda^{-1}_{1/8,2}(Q) <= 2 max_{R in descendantsAtScale Q n} lambda^{-1}_{1/16,2}(R), gap constant G(1/8,1/16,2) = 1 + 3^{-1/8} <= 2). This is exactly the accounting recorded in the header of FiniteQTransfer.lean.

• The entropy of the 3^{d(m-n)} translates is NOT absorbed by an adjusted constant. ABK26 says "the constant c is adjusted to absorb the polynomial factor 3^{d(m-n)} from the union bound". A dimension-only c cannot do that: the loss grows with m - n while the double exponential exp(-exp(c E^{-2} gamma^{-1})) does not. Accordingly the headline theorem here, measureReal_coarseEllipticityFailure_le_of_translateCoarseBounds, is stated with no gate at all and carries the loss,

  P[ lambda^{-1}_{1/8,2}(square_m; a_n) sigmabar_{n-1} > 2 . 2 Ccg ]
    <= 3^{d(m-n)} exp( - exp( (1/4) Ccg^{-1} E^{-2} gamma^{-1} ) ) ,
  

  and the passage to the printed shape is a separate, explicitly gated step (..._of_absorb, ..._printed_of_gap), whose gate

  d (m - n) log 3 + T <= exp( (1/4) Ccg^{-1} E^{-2} gamma^{-1} )
  

  is the exact and only inequality the absorption needs. Nothing in this module hides it: the loss-carrying theorem is unconditional, and every printed-shape statement carries the gate as a named binder.

The size of the gate

The gate above is a genuine restriction on m - n, not a constant adjustment. Two remarks fix its size.

• It is much weaker than the self-consistent restriction imposed on the oscillation branch at n < m (3^{5(m-n)_+} <= c c_star gamma^{-1}, i.e. m - n <~ log_3(gamma^{-1})/5), because here m - n may grow like exp(c E^{-2} gamma^{-1}), doubly exponentially larger.
• The union bound wins because the per-translate tail is doubly exponential while the loss is only exponential in m - n; that is the whole reason a gate on m - n suffices and no adjustment of the constant is needed.

The two conditional binders

• hcg is the conclusion of p.cg.ellipticity.bounds at every translate R in descendantsAtScale Q n, at sigma = 1/2, s = 1/16, q = 2, in the exact shape of the frozen Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds conclusion but with the centered observable Observable.cutoffLowerEllipticityInv M n L ... replaced by the general-cube observable cubeLowerEllipticityInv M .... Two things are carried by this single binder, both of them steps the manuscript itself takes:

  1. the helper keeps the frozen theorem's specialization explicit as a conditional A binder, exactly as in BadEventLemmaCases.lean; the frozen theorem is now proved and may discharge the centered instance in a downstream assembly;
  2. the manuscript applies the proposition at each translate z + square_n, which is its own stationarity reduction; the frozen statement is at the centered cube. On the centered cube R = originCube d n the two observables agree almost everywhere (cubeLowerEllipticityInv_ae_eq_cutoffLowerEllipticityInv); note however that this a.e. identification does NOT by itself transport the frozen conclusion to this binder even at that one translate, because IsLowerIntegerFamilyOrliczWithWitness.dominates is a pointwise (∀ ω) clause, which an a.e. route cannot reach. Both halves are resolved below.
     • Centered. The exported general-cube and centered observables both reduce pointwise to the same literal by cubeLowerEllipticityInv_eq_literal, Observable.cutoffLowerEllipticityInv_eq_literal, and cubeLowerEllipticityInvLiteral_originCube. Hence the family relation transports with the same witness and no null-set surgery.
     • Since the observable bodies are the literals clamped at 0, the exported observables carry pointwise information, and the proved pathwise covariance LambdaCovariance.lambdaSq_cutoff_translateCutoffSample applies to them directly: cubeLowerEllipticityInv M s hs q omega equals the centered observable at scale R.scale read at the translated sample (ObservableSwapPayoff.cubeLowerEllipticityInv_translateCutoffSample). With the law invariance Cutoff.map_translateCutoffSample_cutoffSampleLaw this produces the WHOLE ∀ R ∈ descendantsAtScale Q n binder from a SINGLE centered instance at scale n (ObservableSwapPayoff's isLowerIntegerFamilyOrlicz_cubeLowerEllipticityInv_forall_descendant), which is precisely the manuscript's stationarity reduction. The binder remains as stated because this module exposes the translated statement rather than assembling its upstream input. The frozen theorem discharges the centered instance, and the transport is what is proved here. The exponent is 1/16, not the printed 1/8, by the q = infinity reading described above. 1/16 lies in the frozen s-window Set.Icc (gamma/2 + exp(-Ccg^{-1} E^{-2} gamma^{-1})) 1 exactly when gamma/2 + exp(-Ccg^{-1} E^{-2} gamma^{-1}) <= 1/16, the t = 1/16 analogue of the proved s = 1/8 gate; that gate is a precondition of the frozen theorem, discharged where the binder is discharged, and therefore appears nowhere here.

• hgamma : gamma <= 1/16 makes the frozen deterministic profile lowerEllipticityProfile Ccg gamma (1/16) 2 = Ccg (1/16) (1/8 - gamma)^{-1} at most Ccg. It is not an addition: gamma_le_one_sixteenth_of_admissible derives it from the manuscript's own admissibility e.bad.event.admissibility at the dimension-only constant badEventOscAdmissibleConst, exactly as the proved n >= m branch derives gamma <= 1/8 (both come from gamma <= E^{-5} <= 1/32).

Main results

• lowerEllipticityProfile_exponentTwo_eq, lowerEllipticityProfile_exponentTwo_sixteenth_le, gamma_le_one_sixteenth_of_admissible: the deterministic profile at s = 1/16.
• cubeLowerEllipticityInv_le_two_mul_finsetSupReal_ae: the transfer, at the observables (stated almost everywhere; the underlying fact is in fact pointwise --- see the structure note at that theorem).
• measureReal_translateCoarseEllipticityTail_le: the per-translate tail.
• measureReal_coarseEllipticityFailure_le_of_translateCoarseBounds: the branch, loss-carrying and gate-free.
• measureReal_coarseEllipticityFailure_le_of_absorb, measureReal_coarseEllipticityFailure_le_printed_of_gap: the printed shape, under the explicit entropy gate.

References

• ABK26, l.bad.event.lemma; the case n < m; the recombined display.
• ABK26, p.cg.ellipticity.bounds.
• ABK26, l.maximums.Gamma.s.

The frozen deterministic profile at q = 2

theorem Algsuperdiff.Section3.Provider.BadEvents.lowerEllipticityProfile_exponentTwo_sixteenth_le {Ccg gamma : ℝ} (hCcg : 0 < Ccg) (hgamma : gamma ≤ 1 / 16) : lowerEllipticityProfile Ccg gamma (1 / 16) exponentTwo ≤ Ccg

At gamma <= 1/16 the frozen deterministic profile at the exponent t = 1/16 is below the frozen constant itself, which is what the manuscript's threshold 2 C_{(e.cg.ellip.lower)} needs. This is the t = 1/16 analogue of the proved lowerEllipticityProfile_exponentTwo_le.

theorem Algsuperdiff.Section3.Provider.BadEvents.gamma_le_one_sixteenth_of_admissible {d : ℕ} (M : ABKModel d) {Ccg E : ℝ} (hadm : badEventOscAdmissibleConst d Ccg ≤ E * Disorder.cstar M) (hgammaE : M.gamma ≤ E ^ (-5)) : M.gamma ≤ 1 / 16

The manuscript's own admissibility e.bad.event.admissibility, at the dimension-only constant badEventOscAdmissibleConst, implies gamma <= 1/16 (indeed gamma <= 1/32). Same derivation as the proved gamma_le_one_eighth_of_admissible, read at the exponent.

The transfer at the observable level

ErrorComparison.lambdaSq_eighth_inv_le_two_mul_max_descendants_sixteenth is a statement about the literal Ch02.lambdaSq of a triadic coefficient family, and holds pointwise in the sample.

The observable bodies are the literals clamped at 0, so cubeLowerEllipticityInv M Q n s hs q is cubeLowerEllipticityInvLiteral M Q n s q on the source range s > 0 (cubeLowerEllipticityInv_eq_literal), and the transfer descends at every sample point. The same applies to the a.e. route of LambdaTransfer.lean.

theorem Algsuperdiff.Section3.Provider.BadEvents.cubeLowerEllipticityInv_le_two_mul_finsetSupReal_ae {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), cubeLowerEllipticityInv M Q n (1 / 8) cubeLowerEllipticityInv_le_two_mul_finsetSupReal_ae._proof_1 exponentTwo omega ≤ 2 * HCPolySupport.Book.Ch02.finsetSupReal (HCPolySupport.descendantsAtScale Q n) fun (R : HCPolySupport.TriadicCube d) => cubeLowerEllipticityInv M R n (1 / 16) cubeLowerEllipticityInv_le_two_mul_finsetSupReal_ae._proof_2 exponentTwo omega

The transfer, at the observables. Almost surely (in fact at every sample point — see the structure note above),

lambda^{-1}_{1/8,2}(square_m; a_n)
  <= 2 max_{R in descendantsAtScale Q n} lambda^{-1}_{1/16,2}(R; a_n) ,

The per-translate tail

In the manuscript, p.cg.ellipticity.bounds at scale n, applied at the translate z + square_n, gives the weak-Orlicz bound whose tail at the level Ccg is the printed double exponential. The argument is the proved one of BadEventLemmaCases.lean, read at the translate and at the exponent.

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_translateCoarseEllipticityTail_le {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 1 ≤ Ccg) (R : HCPolySupport.TriadicCube d) {n : ℤ} {E : ℝ} (hgamma : M.gamma ≤ 1 / 16) (hcg : Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - 1 / 2) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => cubeLowerEllipticityInv M R L (1 / 16) cubeLowerEllipticityInv_le_two_mul_finsetSupReal_ae._proof_2 exponentTwo omega * ↑(Annealed.sigmaBar M (n - 1))) (n - 1) (lowerEllipticityProfile Ccg M.gamma (1 / 16) exponentTwo) (Real.exp (-(Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹)))) : (↑(Cutoff.cutoffSampleLaw M)).real {omega : Cutoff.CutoffSample d | 2 * Ccg < cubeLowerEllipticityInv M R n (1 / 16) cubeLowerEllipticityInv_le_two_mul_finsetSupReal_ae._proof_2 exponentTwo omega * ↑(Annealed.sigmaBar M (n - 1))} ≤ Real.exp (-Real.exp (1 / 4 * (Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹)))

The per-translate tail (ABK26). At each scale-n translate R, the coarse-graining input at the exponent t = 1/16 gives

P[ lambda^{-1}_{1/16,2}(R; a_n) sigmabar_{n-1} > 2 Ccg ]
  <= exp( - exp( (1/4) Ccg^{-1} E^{-2} gamma^{-1} ) ) .

The subcube cover of the failure event

theorem Algsuperdiff.Section3.Provider.BadEvents.coarseEllipticityFailure_ae_subset_biUnion {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (Q : HCPolySupport.TriadicCube d) {n : ℤ} (hnm : n < Q.scale) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), omega ∈ coarseEllipticityFailure M (2 * Ccg) Q n → omega ∈ ⋃ R ∈ HCPolySupport.descendantsAtScale Q n, {omega : Cutoff.CutoffSample d | 2 * Ccg < cubeLowerEllipticityInv M R n (1 / 16) cubeLowerEllipticityInv_le_two_mul_finsetSupReal_ae._proof_2 exponentTwo omega * ↑(Annealed.sigmaBar M (n - 1))}

The subcube decomposition of the failure event (ABK26), almost surely: at the re-based constant 2 Ccg the printed-cube coarse-ellipticity failure event is covered by the scale-n translate events at the bare level 2 Ccg.

The branch, loss-carrying and gate-free

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_coarseEllipticityFailure_le_of_translateCoarseBounds {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 1 ≤ Ccg) (Q : HCPolySupport.TriadicCube d) {n : ℤ} {E : ℝ} (hnm : n < Q.scale) (hgamma : M.gamma ≤ 1 / 16) (hcg : ∀ R ∈ HCPolySupport.descendantsAtScale Q n, Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - 1 / 2) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => cubeLowerEllipticityInv M R L (1 / 16) cubeLowerEllipticityInv_le_two_mul_finsetSupReal_ae._proof_2 exponentTwo omega * ↑(Annealed.sigmaBar M (n - 1))) (n - 1) (lowerEllipticityProfile Ccg M.gamma (1 / 16) exponentTwo) (Real.exp (-(Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹)))) : (↑(Cutoff.cutoffSampleLaw M)).real (coarseEllipticityFailure M (2 * Ccg) Q n) ≤ ↑(HCPolySupport.descendantsAtScale Q n).card * Real.exp (-Real.exp (1 / 4 * (Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹)))

The case n < m of the coarse-ellipticity branch (ABK26), with the union loss carried:

P[ lambda^{-1}_{1/8,2}(square_m; a_n) sigmabar_{n-1} > 2 . (2 Ccg) ]
  <= 3^{d(m-n)} exp( - exp( (1/4) Ccg^{-1} E^{-2} gamma^{-1} ) ) .

There is no hypothesis on m - n: the cardinality of the translate set appears in the conclusion, where the manuscript puts it into an "adjusted" constant c, which a dimension-only c cannot absorb. The passage to the printed shape is measureReal_coarseEllipticityFailure_le_of_absorb.

The constant 2 Ccg at which the failure event is read is the Ccg re-basing (gap route, G <= 2); hcg is the coarse-graining input at every translate, at the exponent t = 1/16.

The absorption of the union loss

theorem Algsuperdiff.Section3.Provider.BadEvents.log_card_descendantsAtScale {d : ℕ} (Q : HCPolySupport.TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) : Real.log ↑(HCPolySupport.descendantsAtScale Q n).card = ↑d * (↑Q.scale - ↑n) * Real.log 3

The logarithm of the union loss is the manuscript's own d (m - n) log 3.

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_coarseEllipticityFailure_le_of_absorb {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 1 ≤ Ccg) (Q : HCPolySupport.TriadicCube d) {n : ℤ} {E T : ℝ} (hnm : n < Q.scale) (hgamma : M.gamma ≤ 1 / 16) (hcg : ∀ R ∈ HCPolySupport.descendantsAtScale Q n, Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - 1 / 2) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => cubeLowerEllipticityInv M R L (1 / 16) cubeLowerEllipticityInv_le_two_mul_finsetSupReal_ae._proof_2 exponentTwo omega * ↑(Annealed.sigmaBar M (n - 1))) (n - 1) (lowerEllipticityProfile Ccg M.gamma (1 / 16) exponentTwo) (Real.exp (-(Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹)))) (hAbsorb : Real.log ↑(HCPolySupport.descendantsAtScale Q n).card + T ≤ Real.exp (1 / 4 * (Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹))) : (↑(Cutoff.cutoffSampleLaw M)).real (coarseEllipticityFailure M (2 * Ccg) Q n) ≤ Real.exp (-T)

The absorption of the union loss. If the entropy of the 3^{d(m-n)} translates fits under the per-translate double exponent with room T to spare, the branch is delivered at the level exp(-T).

The hypothesis hAbsorb is the inequality the manuscript's needs and does not state; by log_card_descendantsAtScale it reads

d (m - n) log 3 + T <= exp( (1/4) Ccg^{-1} E^{-2} gamma^{-1} ) .

It is a restriction on the scale separation m - n, not a constant adjustment.

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_coarseEllipticityFailure_le_printed_of_gap {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 1 ≤ Ccg) (Q : HCPolySupport.TriadicCube d) {n : ℤ} {E : ℝ} (hnm : n < Q.scale) (hgamma : M.gamma ≤ 1 / 16) (hcg : ∀ R ∈ HCPolySupport.descendantsAtScale Q n, Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - 1 / 2) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => cubeLowerEllipticityInv M R L (1 / 16) cubeLowerEllipticityInv_le_two_mul_finsetSupReal_ae._proof_2 exponentTwo omega * ↑(Annealed.sigmaBar M (n - 1))) (n - 1) (lowerEllipticityProfile Ccg M.gamma (1 / 16) exponentTwo) (Real.exp (-(Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹)))) (hgap : ↑d * (↑Q.scale - ↑n) * Real.log 3 + Real.exp (1 / 8 * (Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹)) ≤ Real.exp (1 / 4 * (Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹))) : (↑(Cutoff.cutoffSampleLaw M)).real (coarseEllipticityFailure M (2 * Ccg) Q n) ≤ Real.exp (-Real.exp (1 / 8 * (Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹)))

The printed shape of the branch, under the explicit entropy gate. With T = exp((1/8) Ccg^{-1} E^{-2} gamma^{-1}) the conclusion is the manuscript's own display, at the dimension-only constant c = Ccg^{-1}/8 (the proved n >= m branch delivers Ccg^{-1}/4, which is stronger, so the two branches combine at Ccg^{-1}/8).

The gate is stated in the manuscript's own variables: m = Q.scale, n, and d.