Capped cross ledger, part 1: entity integrals and the graded reduction

This file isolates the per-entity integral

J(e) = ∫ (left chain)·(right chain)·(cross covariance of e) dp

of a pure-cross contraction entity, records its integrability, and proves the graded reduction: the capped cross ledger R324CappedCrossLedger follows from a per-entity bound C^m·L^{grade e} together with the graded count ∑_e L^{grade e} ≤ C^m·L^{m-1} (r324CappedCrossLedger_of_grading).

The grading is forced. An ungraded per-entity ceiling C^m·L^{m-1} (which is sharp: the identity entity really is of that size, and by r324PermCross_integral_crossDensity_ge every entity is ≥ c^m) multiplied by the m! entity count only gives C^m·L^{2(m-1)} once m! ≈ L^{m-1} at the top of the capped range — over budget by L^{m-1}. So a proof must exploit that only ≈ C^m entities carry the full window power. Exactly at m = 3 the count 3! = 6 is itself ≤ C^m, so there the ungraded bound suffices (r324CappedCrossGradingBound_of_entityBound), which is why the m = 3 calibration is the honest first target.

The per-entity integral

noncomputable def Anderson4D.r324CappedCrossEntityIntegral (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (e : MomentContraction m) : ℝ

The physical integral of one pure-cross contraction entity.

Equations

• Anderson4D.r324CappedCrossEntityIntegral ρ ε m e = ∫ (p : Anderson4D.R324PhysicalPoint m), Anderson4D.r324CappedCrossEntityDensity ρ ε m e p ∂Anderson4D.r324PhysicalMeasure m

theorem Anderson4D.r324CappedCrossEntityDensity_integrable (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} {e : MomentContraction m} (he : R324LedgerThreeAllCrossEntity e) : MeasureTheory.Integrable (fun (p : R324PhysicalPoint m) => r324CappedCrossEntityDensity ρ ε m e p) (r324PhysicalMeasure m)

Every pure-cross entity density is integrable on the physical space (proved: it is the density of one permutation summand).

theorem Anderson4D.r324CappedCrossEntityIntegral_nonneg (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (e : MomentContraction m) : 0 ≤ r324CappedCrossEntityIntegral ρ ε m e

theorem Anderson4D.r324CappedCross_allCross_of_mem_permEntities {m : ℕ} {e : MomentContraction m} (he : e ∈ r324LedgerThreePermEntities m) : R324LedgerThreeAllCrossEntity e

Membership in the permutation entities forces the pure-cross shape.

theorem Anderson4D.r324CappedCross_integral_eq_sum (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} {F : Finset (MomentContraction m)} (hF : ∀ e ∈ F, R324LedgerThreeAllCrossEntity e) : ∫ (p : R324PhysicalPoint m), r324LedgerThreeCrossDensity ρ ε m F p ∂r324PhysicalMeasure m = ∑ e ∈ F, r324CappedCrossEntityIntegral ρ ε m e

The fibre integral is the entity-wise sum of entity integrals.

The grading Prop

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

The graded per-entity ledger. At each capped order there is a grade function on the pure-cross entities such that

• each entity integral is ≤ C^m·L^{grade e}, and
• the graded count obeys ∑_e L^{grade e} ≤ C^m·L^{m-1}.

The identity-like entities saturate grade = m-1 but number only ≈ C^m; the deranged ones lose window resonance and carry a strictly smaller grade. This is the exact content that a uniform per-entity bound cannot supply.

Equations

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

def Anderson4D.R324CappedCrossGradingBound (ρ : SmoothCutoff) (C : ℝ) : Prop

The grading Prop at every capped order.

Equations

• Anderson4D.R324CappedCrossGradingBound ρ C = ∀ (m : ℕ), Anderson4D.R324CappedCrossGradingBoundAt ρ C m

def Anderson4D.R324CappedCrossLedgerAt (ρ : SmoothCutoff) (K : ℝ) (m : ℕ) : Prop

The capped cross ledger at one fixed order.

Equations

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

theorem Anderson4D.r324CappedCrossLedger_of_at {ρ : SmoothCutoff} {K : ℝ} (h : ∀ (m : ℕ), R324CappedCrossLedgerAt ρ K m) : R324CappedCrossLedger ρ K

The order-indexed ledgers assemble to the exact proved Prop.

theorem Anderson4D.r324CappedCrossLedgerAt_of_gradingAt {ρ : SmoothCutoff} {C : ℝ} {m : ℕ} (hC : 0 ≤ C) (h : R324CappedCrossGradingBoundAt ρ C m) : R324CappedCrossLedgerAt ρ (C * C) m

The graded reduction at one order. The grading Prop delivers the capped cross ledger at the squared constant.

theorem Anderson4D.r324CappedCrossLedger_of_grading {ρ : SmoothCutoff} {C : ℝ} (hC : 0 ≤ C) (h : R324CappedCrossGradingBound ρ C) : R324CappedCrossLedger ρ (C * C)

The graded reduction, all orders. The grading Prop delivers the exact proved R324CappedCrossLedger at the squared constant.

theorem Anderson4D.mainConditional_of_crossGrading_capped {M : NoiseModel} {ρ : SmoothCutoff} (hgrade : ∃ (C : ℝ), 0 ≤ C ∧ R324CappedCrossGradingBound ρ C) (hmixed : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedMixedLedger ρ K) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324CappedBracketLedger ρ K) : MainConditional M ρ

The endpoint. The graded cross ledger plugs straight into the proved capped conditional main theorem: MainConditional follows from the grading Prop together with the two other capped residual Props.

The ungraded per-entity bound and its exact range of validity

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

The ungraded per-entity ledger: every pure-cross entity integral obeys the full window bound C^m·L^{m-1}. This is sharp (the identity entity saturates it) and is the object the m = 3 calibration evaluates.

Equations

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

theorem Anderson4D.r324CappedCross_card_permEntities (m : ℕ) : (r324LedgerThreePermEntities m).card = m.factorial

The number of pure-cross entities is m!.

theorem Anderson4D.r324CappedCrossGradingBoundAt_of_entityBoundAt {ρ : SmoothCutoff} {C D : ℝ} {m : ℕ} (hC : 0 ≤ C) (hD : 0 ≤ D) (hfac : ↑m.factorial ≤ D ^ m) (h : R324CappedCrossEntityBoundAt ρ C m) : R324CappedCrossGradingBoundAt ρ (max C D) m

The ungraded bound funds the grading exactly when the factorial count at this order is geometric. With the constant D absorbing m! this gives the grading Prop with the flat grade m-1. At m = 3 the hypothesis holds with D = 2 (3! = 6 ≤ 8); for large m it fails for every fixed D, which is the precise reason the grading is unavoidable beyond the lowest orders.

theorem Anderson4D.r324CappedCrossLedgerAt_three_of_entityBoundAt {ρ : SmoothCutoff} {C : ℝ} (hC : 2 ≤ C) (h : R324CappedCrossEntityBoundAt ρ C 3) : R324CappedCrossLedgerAt ρ (C * C) 3

The m = 3 slice needs no grading. The entity count 3! = 6 is already geometric, so the ungraded per-entity bound closes the capped cross ledger at order three outright.