DisplaySlots

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

The two lattice slots of the clause-(i) representative display

RepresentativeTransfer.clauseOne_representative_display transports the pointwise literal estimate of ClauseOne to the almost-sure, [0,infinity]-valued display at the representative observables, and carries two named slots:

• hE2dom — the real (2,2)-atom family is dominated by the display's [0,infinity]-valued supremum over the lattice annulus 3^n Z^d ∩ (□_j ∖ □_{j−1});
• hG1bdom — the single shell sum Σ_v 3^{−(s/2)v} A(m−v)^2 is dominated by the display's n-then-k double block sum.

Both are bookkeeping, not source gaps, and this module discharges them at the honest lattice carriers.

What is proved

• ofReal_fmax_le_iSup — the generic transfer: the 0-floored finite maximum over a Finset of lattice indices, sent into [0,infinity], is below the [0,infinity]-valued supremum over any set containing those indices. No nonemptiness is needed (the empty maximum is 0).
• annularErrorLatticeMax, shellW2InfLatticeMax, shellBlockLatticeReal — the real families the display's two slots are instantiated at, and their dominations ofReal_annularErrorLatticeMax_le, ofReal_shellBlockLatticeReal_sq_le.
• ofReal_shellSingleSum_le_clauseOneTermFour — the hG1bdom slot at constant 1, by the distinct-slot injection v ↦ n = m − v: the shell k = m − v of the single sum is placed in the n = m − v slot of the double sum, where it is one summand of Σ_{k ∈ [n−1, m]} and carries exactly the single sum's own weight 3^{−(s/2)v}. The assignment is injective in v, so no slot is used twice.
• clauseOne_representative_display_latticeMax — the display with both slots discharged, i.e. depending only on the pointwise chain hbound.

References

• ABK26, p.mathcalE.annular.decomp clause (i).

Part A -- the generic maximum transfers

theorem Algsuperdiff.Section4.Provider.Annular.ofReal_fmax_le_iSup {iota : Type u_1} {S : Finset iota} {T : Set iota} (hST : ∀ i ∈ S, i ∈ T) (f : iota → ℝ) : ENNReal.ofReal (Proportion.fmax S f) ≤ ⨆ (i : ↑T), ENNReal.ofReal (f ↑i)

No nonemptiness enters — at the empty index set the left side is 0.

Part C -- the hE2dom slot

noncomputable def Algsuperdiff.Section4.Provider.Annular.annularErrorLatticeMax {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) (j n : ℤ) : ℝ

The (2,2) atom family of the display, as an honest finite maximum. The lattice maximum over 3^n Z^d ∩ (□_j ∖ □_{j−1}) of the squared annular error observable, 0-floored (which changes nothing: the entries are squares).

Equations

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

theorem Algsuperdiff.Section4.Provider.Annular.annularErrorLatticeMax_nonneg {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) (j n : ℤ) : 0 ≤ annularErrorLatticeMax M s omega j n

theorem Algsuperdiff.Section4.Provider.Annular.le_annularErrorLatticeMax {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) {j n : ℤ} (hn : n ≤ j) {v : Fin d → ℤ} (hv : v ∈ Support.latticeAnnulusSet d n j (j - 1)) : Support.annularErrorObservable M n s (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint n v) omega) ^ 2 ≤ annularErrorLatticeMax M s omega j n

Every lattice atom is below the maximum: the form a producer of the ClauseOne chain consumes.

theorem Algsuperdiff.Section4.Provider.Annular.ofReal_annularErrorLatticeMax_le {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) {j n : ℤ} (hn : n ≤ j) : ENNReal.ofReal (annularErrorLatticeMax M s omega j n) ≤ ⨆ (v : ↑(Support.latticeAnnulusSet d n j (j - 1))), ENNReal.ofReal (Support.annularErrorObservable M n s (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint n ↑v) omega) ^ 2)

The hE2dom slot. The finite lattice maximum, sent into [0,infinity], is below the display's [0,infinity]-valued lattice supremum.

Part D -- the hG1bdom slot

noncomputable def Algsuperdiff.Section4.Provider.Annular.shellBlockLatticeAtom {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (k : ℤ) : ENNReal

The [0,infinity]-valued shell block atom of the display's fourth term: 3^{(2−γ)k} max_{z ∈ 3^k Z^d ∩ □_m} ‖j_k‖_{W^{2,∞}(z+□_k)}.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Annular.clauseOneTermFourSlot {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) (n : { n : ℤ // n ≤ m }) : ENNReal

The n-slot of the display's fourth term.

Equations

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

theorem Algsuperdiff.Section4.Provider.Annular.clauseOneTermFour_eq_tsum {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) : clauseOneTermFour M m s omega = ∑' (n : { n : ℤ // n ≤ m }), clauseOneTermFourSlot M m s omega n

theorem Algsuperdiff.Section4.Provider.Annular.ofReal_shellSingleSum_le_clauseOneTermFour {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) {A : ℤ → ℝ} (hA : ∀ k ≤ m, ENNReal.ofReal (A k ^ 2) ≤ shellBlockLatticeAtom M m omega k ^ 2) : ENNReal.ofReal (∑' (v : ℕ), 3 ^ (-(↑s / 2) * ↑v) * A (m - ↑v) ^ 2) ≤ clauseOneTermFour M m s omega

The hG1bdom slot, at constant 1.

The single shell sum Σ_{v ≥ 0} 3^{−(s/2)v} A(m−v)^2 is dominated by the display's double block sum by the distinct-slot injection v ↦ n = m − v:

• the n-slot of the fourth term weighs 3^{−(s/2)(m−n)}, which at n = m − v is exactly the single sum's own weight 3^{−(s/2)v};
• its inner sum runs over k ∈ [n−1, m] = [m−v−1, m], which contains k = m − v, so the single sum's v-th atom is one of its summands;
• v ↦ m − v is injective, so no slot of the double sum is used twice.

No constant is lost. The per-shell hypothesis hA is the atom-level domination, discharged at the honest lattice carrier by ofReal_shellBlockLatticeReal_sq_le.

Part E -- the shell family at the honest lattice carrier

noncomputable def Algsuperdiff.Section4.Provider.Annular.shellW2InfLatticeMax {d : ℕ} (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (k : ℤ) : ℝ

The lattice maximum of the shell W^{2,∞} norms over 3^k Z^d ∩ □_m.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.Annular.shellBlockLatticeReal {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (k : ℤ) : ℝ

The real shell block family A(k) = 3^{(2−γ)k} max_z ‖j_k‖_{W^{2,∞}(z+□_k)} of the single shell sum.

Equations

• Algsuperdiff.Section4.Provider.Annular.shellBlockLatticeReal M m omega k = 3 ^ ((2 - M.gamma) * ↑k) * Algsuperdiff.Section4.Provider.Annular.shellW2InfLatticeMax m omega k

theorem Algsuperdiff.Section4.Provider.Annular.shellW2InfLatticeMax_nonneg {d : ℕ} (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (k : ℤ) : 0 ≤ shellW2InfLatticeMax m omega k

theorem Algsuperdiff.Section4.Provider.Annular.shellBlockLatticeReal_nonneg {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (k : ℤ) : 0 ≤ shellBlockLatticeReal M m omega k

theorem Algsuperdiff.Section4.Provider.Annular.ofReal_shellBlockLatticeReal_le {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {k : ℤ} (hk : k ≤ m) : ENNReal.ofReal (shellBlockLatticeReal M m omega k) ≤ shellBlockLatticeAtom M m omega k

The real shell block family is dominated by the [0,infinity]-valued atom.

theorem Algsuperdiff.Section4.Provider.Annular.ofReal_shellBlockLatticeReal_sq_le {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) {k : ℤ} (hk : k ≤ m) : ENNReal.ofReal (shellBlockLatticeReal M m omega k ^ 2) ≤ shellBlockLatticeAtom M m omega k ^ 2

The squared form, i.e. the hA hypothesis of ofReal_shellSingleSum_le_clauseOneTermFour at the honest lattice carrier.

Part F -- the display with both slots discharged

theorem Algsuperdiff.Section4.Provider.Annular.clauseOne_representative_display_latticeMax {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (s : { s : ℝ // 0 < s }) (Event : Set (Section3.Cutoff.CutoffSample d)) {C : ℝ} (hC0 : 0 ≤ C) (hbound : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Event → ∀ (L : ℤ), m ≤ L → IsClauseOneBound (Support.fluxCorrectedError M L m (↑s) omega ^ 2) (annDouble m fun (j n : ℤ) => 3 ^ (-(↑s * ↑(m - n))) * annularErrorLatticeMax M s omega j n) (M.gamma ^ 2 * |Real.log M.gamma| ^ 4) (gradTailSq M m omega) (∑' (v : ℕ), 3 ^ (-(↑s / 2) * ↑v) * shellBlockLatticeReal M m omega (m - ↑v) ^ 2) (↑s) (Section3.Disorder.cstar M) M.gamma C) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), Event.indicator (Support.fluxCorrectedErrorObservableSqSup M m s) omega ≤ ENNReal.ofReal (C * ↑s) * clauseOneTermOne M m s omega + ENNReal.ofReal (C * (↑s)⁻¹ ^ 3 * (Section3.Disorder.cstar M)⁻¹ ^ 4 * M.gamma ^ 2 * |Real.log M.gamma| ^ 4) + ENNReal.ofReal (C * (↑s)⁻¹ ^ 2 * (Section3.Disorder.cstar M)⁻¹ * M.gamma) * clauseOneTermThree M m omega + ENNReal.ofReal (C * (↑s)⁻¹ ^ 2 * (Section3.Disorder.cstar M)⁻¹ * M.gamma) * clauseOneTermFour M m s omega

The clause-(i) representative display, at the lattice maxima.

clauseOne_representative_display with its two slots discharged: the (2,2) atom family is the finite lattice maximum annularErrorLatticeMax over 3^n Z^d ∩ (□_j ∖ □_{j−1}), and the single shell family is the finite lattice maximum shellBlockLatticeReal over 3^k Z^d ∩ □_m. Only the pointwise chain hbound — the output of clauseOne_bound at each L — remains.

The remaining hypothesis is a conditional A obligation, not a source premise; no source node is claimed, realized or closed.