Necessity of the order cap in the R-324 re-base

The following uncapped bridge momentRefinedIntegratedReductionOutputAt_of_generalPeelFibreLogBound consumes the per-fibre ledger R324GeneralPeelFibreLogBound at every order m ≥ 1 with no cap. This file proves that the uncapped residual ledger R324GeneralPeelLedgerFromThree cannot hold — the factorial fibre floor refutes the cancellation-carrying term-sum ledger itself, not merely its norm-inside density majorization:

• the bridge's summed object momentRefinedDeterministicTermSum is the unnormalized sum of deterministicMomentContractionTerm over a residual-refined fibre; no ∏ mₗ!-type paper normalization discounts the fibre count anywhere in that chain;
• at trivial external modes α = β = 0 the integrand of every entity in the trivial-signature fibre (both pairings extract nothing, so no signed diffFactor appears) is the coercion of a pointwise nonnegative real product — there is no cancellation to hide behind: every term is real and nonnegative (r324CappedRebase_term_trivialSig_nonneg);
• the full m! bijection family lies inside that single signature fibre, which splits into at most 4^{2m} refined fibres, so the ledger's budget K^m·L^{m-1} per refined fibre caps the whole fibre sum by (16K)^m at the admissible scale ε = e⁻¹ (L = 1), while the proved floor r324PermCross_crossDensity_factorial_floor forces at least C₀·m!·c^m — contradiction for large m (r324CappedRebase_generalPeelLedgerFromThree_no_constant).

Consequently the uncapped hypotheses R324LedgerThreeCrossLedger and R324LedgerThreeMixedLedger are incompatible (r324CappedRebase_crossMixed_incompatible). The valid interface therefore caps the order against truncOrder ε.

The trivial signature and its fibre

theorem Anderson4D.r324CappedRebase_signature_id (m : ℕ) : momentWithinHalfEndpointSignature PartialPairing.id PartialPairing.id = (∅, ∅)

The within-half endpoint signature of the identity pairings is the empty pair: nothing is extracted, so there are no interval endpoints.

theorem Anderson4D.r324CappedRebase_extract_nil_of_trivialSig {m : ℕ} {e : MomentContraction m} (h : momentContractionSignature e = (∅, ∅)) : extract e.fst = [] ∧ extract e.snd.fst = []

Any entity realizing the trivial signature has extraction-free pairings in both halves: an extracted interval would contribute a left endpoint to the (empty) signature.

No cancellation at trivial external modes

theorem Anderson4D.r324CappedRebase_detIntegrand_nonneg_of_extract_nil (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} {κ : PartialPairing (Fin m)} (hnil : extract κ = []) (xt : Fin (m + 2) → T4) : 0 ≤ detIntegrand ρ ε m κ xt

With nothing extracted there is no signed diffFactor: the deterministic profile is a plain product of Green factors and covariance factors, hence nonnegative.

noncomputable def Anderson4D.r324CappedRebaseProfile (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (e : MomentContraction m) (p : R324PhysicalPoint m) : ℝ

The phase-free real profile of one contraction entity: the two deterministic within-half profiles against the cross covariance.

Equations

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

theorem Anderson4D.r324CappedRebase_flatten_trivialModes (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (e : MomentContraction m) (p : R324PhysicalPoint m) : r324Flatten (deterministicMomentIntegrand ρ ε m 0 0 e.fst e.snd.fst e.snd.snd) p = ↑(r324CappedRebaseProfile ρ ε e p)

At α = β = 0 every contraction integrand is the coercion of the real profile: all four external characters are 1.

theorem Anderson4D.r324CappedRebase_term_trivialSig_nonneg (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} {e : MomentContraction m} (h : momentContractionSignature e = (∅, ∅)) : deterministicMomentContractionTerm ρ ε m 0 0 e = ↑(∫ (p : R324PhysicalPoint m), r324CappedRebaseProfile ρ ε e p ∂r324PhysicalMeasure m) ∧ 0 ≤ ∫ (p : R324PhysicalPoint m), r324CappedRebaseProfile ρ ε e p ∂r324PhysicalMeasure m

Trivial-signature terms are real and nonnegative at trivial external modes: the frozen contraction term of any entity in the trivial-signature fibre equals the integral of a pointwise nonnegative real product — no cancellation is available.

The trivial-signature fibre sum carries the factorial floor

theorem Anderson4D.r324CappedRebase_fibreSum_ge_crossDensity (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} {F : Finset (MomentContraction m)} (hFcross : ∀ e ∈ F, R324LedgerThreeAllCrossEntity e) : ∃ (T : ℝ), ∑ e ∈ momentContractionFiber m (momentWithinHalfEndpointSignature PartialPairing.id PartialPairing.id), deterministicMomentContractionTerm ρ ε m 0 0 e = ↑T ∧ ∫ (p : R324PhysicalPoint m), r324LedgerThreeCrossDensity ρ ε m F p ∂r324PhysicalMeasure m ≤ T

The trivial-signature fibre sum is real and dominates every pure-cross density integral at trivial modes. No cancellation: all terms of the fibre are nonnegative reals, and the all-cross subfamily contributes exactly its summed density.

Nonexistence of an uncapped constant

theorem Anderson4D.r324CappedRebase_generalPeelLedgerFromThree_no_constant (ρ : SmoothCutoff) : ¬∃ (K : ℝ), 0 ≤ K ∧ R324GeneralPeelLedgerFromThree ρ K

The uncapped per-fibre ledger has no constant. At ε = e⁻¹ the trivial-signature fibre sum at trivial external modes is a sum of nonnegative reals containing the full m! bijection family; the ledger caps it by 4^{2m}·K^m·L^{m-1} = (16K)^m, which the proved factorial floor defeats.

theorem Anderson4D.r324CappedRebase_crossMixed_incompatible (ρ : SmoothCutoff) : ¬((∃ (K : ℝ), 0 ≤ K ∧ R324LedgerThreeCrossLedger ρ K) ∧ ∃ (K : ℝ), 0 ≤ K ∧ R324LedgerThreeMixedLedger ρ K)

The uncapped cross and mixed ledgers cannot both hold: their composition would produce the unavailable uncapped peel ledger.