Factorial obstruction to an uncapped injective cross bound

The uncapped crossIntegral hypothesis for the uniform-branch closure exists_momentRefinedIntegratedReductionOutputAt_of_crossIntegral_and_mixed demands, for a single K = K(ρ) and every order m ≥ 3 and every admissible scale,

∫ (pure-cross fibre density) ≤ K^m |log ε|^{m-1}.

This file proves that no such order-uniform estimate exists. Retaining pairing injectivity does not make the uniform branch valid: injectivity fixes the fibre cardinality at exactly m!, and each of the m! bijection entities carries at least one full covariance mass above the Green floor,

∫ ≥ g₀^{2m+2} · m! · (2π)^{4(m+4)} (r324PermCross_integral_crossDensity_ge),

an ε-uniform bound. At the admissible scale ε = e⁻¹ (where |log ε| = 1) the demanded budget degenerates to K^m, and m! c^m > K^m for large m.

The obstruction is the factorial fibre count itself, which the paper controls because its expansion is truncated at A = ⌊|log ε|⌋ orders (truncOrder) and its §5 permutation-sum machinery is allowed (m!)^{1/2}-type growth (cf. permSumRHS). Any sound uniform-branch interface must either cap the order against |log ε| or budget an explicit factorial factor; R324PermCrossOrderCappedCrossBound records the order-capped form.

theorem Anderson4D.r324PermCross_permEntities_allCross (m : ℕ) (e : MomentContraction m) : e ∈ r324LedgerThreePermEntities m → R324LedgerThreeAllCrossEntity e

Every permutation entity is a pure-cross entity.

theorem Anderson4D.r324PermCross_exists_factorial_beats_pow {c C₀ : ℝ} (hc : 0 < c) (hC₀ : 0 < C₀) (K : ℝ) (N : ℕ) : ∃ (m : ℕ), N ≤ m ∧ K ^ m < C₀ * (↑m.factorial * c ^ m)

Factorial growth defeats every geometric budget: given c > 0 and 0 < C₀, for every K ≥ 0 there are arbitrarily large m with K ^ m < C₀ * (m.factorial * c ^ m).

theorem Anderson4D.r324PermCross_crossIntegral_no_constant (ρ : SmoothCutoff) : ¬∃ (K : ℝ), 0 ≤ K ∧ ∀ {ε : ℝ} (m : ℕ), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 3 ≤ m → ∀ (F : Finset (MomentContraction m)), (∀ e ∈ F, R324LedgerThreeAllCrossEntity e) → ∫ (p : R324PhysicalPoint m), r324LedgerThreeCrossDensity ρ ε m F p ∂r324PhysicalMeasure m ≤ K ^ m * |Real.log ε| ^ (m - 1)

No constant funds the uncapped injectivity-retaining cross bound. The crossIntegral hypothesis of the auxiliary closure exists_momentRefinedIntegratedReductionOutputAt_of_crossIntegral_and_mixed has no witness: at the admissible scale ε = e⁻¹ the full permutation fibre carries m! unit covariance masses above the Green floor, defeating K^m |log ε|^{m-1} at large m.

theorem Anderson4D.r324PermCross_crossDensity_factorial_floor (ρ : SmoothCutoff) : ∃ (c : ℝ) (C₀ : ℝ), 0 < c ∧ 0 < C₀ ∧ ∀ {ε : ℝ} (m : ℕ), 0 < ε → ε ≤ 1 → 1 ≤ m → ∃ (F : Finset (MomentContraction m)), (∀ e ∈ F, R324LedgerThreeAllCrossEntity e) ∧ C₀ * (↑m.factorial * c ^ m) ≤ ∫ (p : R324PhysicalPoint m), r324LedgerThreeCrossDensity ρ ε m F p ∂r324PhysicalMeasure m

The ε-uniform factorial floor of the pure-cross fibre, in the interface variables: at every admissible scale the summed pure-cross density of the full bijection fibre integrates to at least m! · c(ρ)^m with c independent of ε — so any sound cross-case budget must grow at least factorially in the order. (Re-export of r324PermCross_integral_crossDensity_ge with the fibre-side hypotheses of the interface.)

def Anderson4D.R324PermCrossOrderCappedCrossBound (ρ : SmoothCutoff) (K : ℝ) : Prop

Order-capped cross bound: the pure-cross fibre bound with the order capped against the logarithmic budget, exactly matching the paper's truncation A = ⌊|log ε|⌋ (truncOrder). The factorial floor r324PermCross_crossDensity_factorial_floor shows some cap (or an explicit factorial allowance) is necessary; this Prop records the form used by the truncated parametrix estimate.

Equations

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