Clause A from a σ-graded lattice budget

This file proves the asymptotic grading estimate: it turns a per-bijection graded budget on the collapsed lattice sum into the exact proved interface R324CappedCrossGradingBoundAt, hence (through the already proved r324CappedCrossLedger_of_grading and mainConditional_of_crossGrading_capped) into MainConditional.

What the file proves

r324Grade_gradingBoundAt_of_layered : layered grading ⇒ clause A's grading interface, where "layered" means

• grade e ≤ m-1 on the pure-cross entities,
• I(e) ≤ A^m·L^{grade e}, and
• #{e : grade e = j} ≤ A^m·(m-j)! for every j ≤ m-1.

The third clause is the σ-grading proper. Its two ends are exactly what one knows unconditionally: at j = 0 it is the trivial entity count m!, at j = m-1 it is the sharp requirement that only A^m bijections carry the full window power L^{m-1} (the identity entity is one of them, and by r324PermCross_integral_crossDensity_ge every entity is ≥ c^m, so nothing weaker than a count can help). The budget K^m·L^{m-1} of clause A is therefore right as stated: no factorial allowance is needed, because the order cap m ≤ ⌊L⌋ makes m! ≤ m^{m-1} ≤ L^{m-1} (r324Grade_factorial_le_pow), so the flat grade is over budget by exactly one L^{m-1} and each unit of grade must buy back one factor m in the count.

r324Grade_layeredAt_of_collapse : assigned collapse + graded lattice budget + permutation layer count ⇒ layered grading. After the physical→lattice collapse each entity is the zero-sum lattice sum ∑_q W_τ(q) of R324CollapseEntity, and the grade lives on the bijection τ.

r324Grade_mainConditional_of_gradedLattice : the end-to-end composition to MainConditional.

Why the grade must be non-constant, and where it comes from

The arithmetic–geometric route of R324CollapseEntity is provably blind to the grading: r324Col_tsum_latWeight_le bounds every τ by the identity pattern because q ↦ q∘τ is a measure-preserving bijection of the zero-sum sector. The grade must therefore be read off the joint structure of the two suffix-sum families. Power counting on the lattice sum ∑_q ∏ᵢ‖ρ̂(εqᵢ)‖² ∏ⱼ⟨Sⱼ⟩⁻²⟨Sⱼ^τ⟩⁻² identifies it: with m-1 free momenta in ℤ⁴ and 2(m-1) quadratic propagators the sum is exactly log-critical, and one factor L is produced per member of a maximal refinement chain of partitions of {1,…,m} whose blocks are intervals simultaneously for the identity order and for the τ order. The identity has the full chain (grade = m-1); the m = 4 bijection τ = (2,4,1,3) has none but the trivial one (grade = 1), matching the table in R324CappedCrossGrading. The layer count in R324GradePermLayerCount is the combinatorial statement that grade j costs (m-j)! in the count; this is the combinatorial input and is recorded as a hypothesis, not assumed anywhere silently.

Layered grading data

def Anderson4D.R324GradeLayeredAt (ρ : SmoothCutoff) (A : ℝ) (m : ℕ) : Prop

Layered grading at one capped order. A grade on the pure-cross entities, bounded by m-1, with the per-entity window bound and the factorial layer count. This is exactly the input r324Grade_sum_pow_le_of_factorial consumes.

Equations

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

theorem Anderson4D.r324Grade_gradingBoundAt_of_layered {ρ : SmoothCutoff} {A : ℝ} {m : ℕ} (hA : 0 ≤ A) (h : R324GradeLayeredAt ρ A m) : R324CappedCrossGradingBoundAt ρ (2 * A) m

The σ-grading discharge. Layered grading data produce the exact proved grading interface, with the constant doubled. This is the asymptotic content of clause A: the m! entities are re-summed against their grades with no loss beyond 2^m.

The lattice-side inputs

def Anderson4D.R324ColGradedBudgetAt (ρ : SmoothCutoff) (D : ℝ) (m : ℕ) (gradeP : Equiv.Perm (Fin m) → ℕ) : Prop

The graded lattice budget. The zero-sum lattice sum of the bijection τ (the collapsed entity of R324CollapseEntity) obeys the window bound at its own grade. For τ = id the grade is m-1 and this is the proved doubled budget R324ColDoubledBudgetAt; for a bijection with no critical proper subspace the grade is 1.

Equations

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

def Anderson4D.R324ColAssignedCollapseAt (ρ : SmoothCutoff) (C : ℝ) (m : ℕ) : Prop

The physical→lattice collapse with an injective bijection assignment. Same content as R324ColPhysicalCollapseAt, but the bijection attached to an entity is required to be a function of the entity and injective on the m! entities — which is how the collapse is produced (the entity of σ collapses to τ = σ⁻¹). Injectivity is what transports a count on bijections to a count on entities.

Equations

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

theorem Anderson4D.r324Col_physicalCollapseAt_of_assigned {ρ : SmoothCutoff} {C : ℝ} {m : ℕ} (h : R324ColAssignedCollapseAt ρ C m) : R324ColPhysicalCollapseAt ρ C m

An assigned collapse is in particular the proved collapse.

def Anderson4D.R324GradePermLayerCount (A : ℝ) (m : ℕ) (gradeP : Equiv.Perm (Fin m) → ℕ) : Prop

The permutation layer count — the σ-grading's combinatorial clause. Grade j may be carried by at most A^m·(m-j)! bijections. j = 0 is free (m! bijections in all); j = m-1 says only A^m bijections carry the full window power.

Equations

• Anderson4D.R324GradePermLayerCount A m gradeP = ((∀ (τ : Equiv.Perm (Fin m)), gradeP τ ≤ m - 1) ∧ ∀ j ≤ m - 1, ↑{τ : Equiv.Perm (Fin m) | gradeP τ = j}.card ≤ A ^ m * ↑(m - j).factorial)

Assembling the layered grading

theorem Anderson4D.r324Grade_layeredAt_of_collapse {ρ : SmoothCutoff} {C D A : ℝ} {m : ℕ} {gradeP : Equiv.Perm (Fin m) → ℕ} (hC : 0 ≤ C) (hD : 0 ≤ D) (hA : 0 ≤ A) (hcol : R324ColAssignedCollapseAt ρ C m) (hbud : R324ColGradedBudgetAt ρ D m gradeP) (hcnt : R324GradePermLayerCount A m gradeP) : R324GradeLayeredAt ρ (max (C * D) A) m

The lattice route to layered grading. Collapse (with an injective assignment), a graded lattice budget, and the permutation layer count give the layered grading data at the product constant.

End to end

theorem Anderson4D.r324Grade_gradingBound_of_layered {ρ : SmoothCutoff} {A : ℝ} (hA : 0 ≤ A) (h : ∀ (m : ℕ), R324GradeLayeredAt ρ A m) : R324CappedCrossGradingBound ρ (2 * A)

Layered grading at every capped order is the proved grading Prop.

theorem Anderson4D.r324Grade_cappedCrossLedger_of_gradedLattice {ρ : SmoothCutoff} {C D A : ℝ} {gradeP : (m : ℕ) → Equiv.Perm (Fin m) → ℕ} (hC : 0 ≤ C) (hD : 0 ≤ D) (hA : 0 ≤ A) (hcol : ∀ (m : ℕ), R324ColAssignedCollapseAt ρ C m) (hbud : ∀ (m : ℕ), R324ColGradedBudgetAt ρ D m (gradeP m)) (hcnt : ∀ (m : ℕ), R324GradePermLayerCount A m (gradeP m)) : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedCrossLedger ρ K

The capped cross ledger from the σ-graded lattice budget. Collapse with an injective bijection assignment, the graded lattice budget, and the permutation layer count give clause A outright.

theorem Anderson4D.r324Grade_mainConditional_of_gradedLattice {M : NoiseModel} {ρ : SmoothCutoff} {C D A : ℝ} {gradeP : (m : ℕ) → Equiv.Perm (Fin m) → ℕ} (hC : 0 ≤ C) (hD : 0 ≤ D) (hA : 0 ≤ A) (hcol : ∀ (m : ℕ), R324ColAssignedCollapseAt ρ C m) (hbud : ∀ (m : ℕ), R324ColGradedBudgetAt ρ D m (gradeP m)) (hcnt : ∀ (m : ℕ), R324GradePermLayerCount A m (gradeP m)) (hmixed : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedMixedLedger ρ K) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedBracketLedger ρ K) : MainConditional M ρ

The endpoint. The σ-graded lattice budget closes clause A, and with the two other capped residual Props it delivers MainConditional.

Consistency with the proved order-three calibration

theorem Anderson4D.r324Grade_permLayerCount_flat_three : R324GradePermLayerCount 2 3 fun (x : Equiv.Perm (Fin 3)) => 2

The m = 3 slice sits inside the layer criterion. All 3! = 6 bijections carry the full grade m-1 = 2, and the criterion at j = m-1 asks for 6 ≤ A³·(3-2)! = A³, true for A = 2. So the proved order-three route is the top layer of the σ-grading, and the framework does not lose the calibration.