Factorial absorption after the fixed-class inner estimate

This file formalizes the numerical factorial step between paper (5.88) and (5.89). For one (N,X) fiber, write M = m_{N,X} and let S be the number of skipped incoming edges in that fiber. The two square-root factors

√(X^M) · √((XY)^(M-S))

are the algebraic envelope of (X Y^(1/2))^M (XY)^(-S/2). The first is absorbed by the leaf factorials, using X ≤ m_l; the second is absorbed by (M-S)!, using XY ≤ M and the exponential series estimate A^B ≤ exp(A) B!.

theorem Anderson4D.sqrt_pow_of_nonneg (x : ℝ) (n : ℕ) (hx : 0 ≤ x) : √(x ^ n) = √x ^ n

Square roots commute with natural powers on nonnegative real numbers.

This elementary normalization lemma is kept local to the single-scale ledger because the paper writes half-powers while the implementation uses ordinary powers of square roots.

noncomputable def Anderson4D.singleScalePrintedFiberFactor (X Y M S : ℕ) : ℝ

The exact per-fiber factor printed after (5.88):

(X √Y)^M (XY)^(-S/2).

Because S is a natural number, the negative half-power is represented without real-exponent bookkeeping as the S-th power of the inverse square root. The next theorem proves that this literal form is exactly the factorial envelope used below.

Equations

• Anderson4D.singleScalePrintedFiberFactor X Y M S = (↑X * √↑Y) ^ M * (√↑(X * Y))⁻¹ ^ S

noncomputable def Anderson4D.singleScalePrintedRpowFiberFactor (X Y M S : ℕ) : ℝ

The same printed expression with its negative half-power represented literally by Real.rpow.

Equations

• Anderson4D.singleScalePrintedRpowFiberFactor X Y M S = (↑X * √↑Y) ^ M * ↑(X * Y) ^ (-↑S / 2)

theorem Anderson4D.singleScalePrintedFiberFactor_eq_rpow (X Y M S : ℕ) : singleScalePrintedFiberFactor X Y M S = singleScalePrintedRpowFiberFactor X Y M S

The inverse-square-root encoding of (XY)^(-S/2) agrees with the literal Real.rpow notation used at the paper-facing statement boundary.

theorem Anderson4D.singleScalePrintedFiberFactor_eq_envelope (X Y M S : ℕ) (hX : 0 < X) (hY : 0 < Y) (hS : S ≤ M) : singleScalePrintedFiberFactor X Y M S = √(↑X ^ M) * √(↑(X * Y) ^ (M - S))

The printed factor after (5.88) is exactly √(X^M) √((XY)^(M-S)) when the fiber is active and no more than M incoming edges are skipped.

theorem Anderson4D.natCast_pow_le_exp_mul_factorial (A B : ℕ) : ↑A ^ B ≤ Real.exp ↑A * ↑B.factorial

The elementary exponential-series inequality used after paper (5.88).

theorem Anderson4D.sqrt_pow_le_two_pow_mul_prod_sqrt_factorial {α : Type u_1} (s : Finset α) (q : α → ℕ) (X M : ℕ) (hX : ∀ a ∈ s, X ≤ q a) (hsum : ∑ a ∈ s, q a = M) : √(↑X ^ M) ≤ 2 ^ M * ∏ a ∈ s, √↑(q a).factorial

The factor √(X^M) is absorbed by the product of leaf factorials at an exponential cost. This is the quantitative form of m_l ∼ X needed here; only the lower bound X ≤ m_l and the exact mass ledger are used.

theorem Anderson4D.sqrt_xy_pow_sub_le_exp_mul_sqrt_factorial (X Y M S : ℕ) (hXY : X * Y ≤ M) : √(↑(X * Y) ^ (M - S)) ≤ Real.exp ↑M * √↑(M - S).factorial

The factor √((XY)^(M-S)) is absorbed by √((M-S)!). The intentionally coarse cost exp(M) is uniform in S.

noncomputable def Anderson4D.singleScaleFactorialEnvelope (X Y M S : ℕ) : ℝ

The per-(N,X) factorial envelope occurring after (5.87).

Equations

• Anderson4D.singleScaleFactorialEnvelope X Y M S = √(↑X ^ M) * √(↑(X * Y) ^ (M - S))

theorem Anderson4D.singleScalePrintedFiberFactor_eq_factorialEnvelope (X Y M S : ℕ) (hX : 0 < X) (hY : 0 < Y) (hS : S ≤ M) : singleScalePrintedFiberFactor X Y M S = singleScaleFactorialEnvelope X Y M S

theorem Anderson4D.singleScaleFactorialEnvelope_le {α : Type u_1} (s : Finset α) (q : α → ℕ) (X Y M S : ℕ) (hX : ∀ a ∈ s, X ≤ q a) (hsum : ∑ a ∈ s, q a = M) (hXY : X * Y ≤ M) : singleScaleFactorialEnvelope X Y M S ≤ (2 * Real.exp 1) ^ M * √↑(M - S).factorial * ∏ a ∈ s, √↑(q a).factorial

Uniform factorial absorption used in the passage (5.88) → (5.89). The explicit universal base is 2e; later paper constants may enlarge it.

theorem Anderson4D.singleScaleNXFactorialEnvelope_le {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) (S : ℕ) : singleScaleFactorialEnvelope a.2 (singleScaleSigma2 Nm mu a).2 (multiplicityNX Nm mu a) S ≤ (2 * Real.exp 1) ^ multiplicityNX Nm mu a * √↑(multiplicityNX Nm mu a - S).factorial * ∏ l ∈ leavesAtNX Nm mu a, √↑(leafMultiplicity mu l).factorial

Specialization to an active (N,X) fiber. This packages exactly the m_l ∈ [X,2X) and XY ≤ m_{N,X} ledgers from (5.75), so the final single-scale assembly does not need to repeat the factorial arithmetic.

theorem Anderson4D.singleScaleNXPrintedFiberFactor_eq_envelope {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) (S : ℕ) (hS : S ≤ multiplicityNX Nm mu a) : singleScalePrintedFiberFactor a.2 (singleScaleSigma2 Nm mu a).2 (multiplicityNX Nm mu a) S = singleScaleFactorialEnvelope a.2 (singleScaleSigma2 Nm mu a).2 (multiplicityNX Nm mu a) S

Active-fiber specialization of the exact printed-factor normalization.

Global (N,X) factorial aggregation

theorem Anderson4D.prod_sqrt_factorial_le_sqrt_factorial_sum {α : Type u_1} (s : Finset α) (f : α → ℕ) : ∏ a ∈ s, √↑(f a).factorial ≤ √↑(∑ a ∈ s, f a).factorial

The product of square-root factorials is bounded by the square-root factorial of the total mass. This is the square-root form of the multinomial divisibility ledger.

theorem Anderson4D.prod_sqrt_factorial_sub_le {α : Type u_1} (s : Finset α) (M S : α → ℕ) (hsub : ∀ a ∈ s, S a ≤ M a) : ∏ a ∈ s, √↑(M a - S a).factorial ≤ √↑(∑ a ∈ s, M a - ∑ a ∈ s, S a).factorial

Square-root factorial deficits aggregate across a finite partition. The pointwise condition is what prevents truncated natural subtraction from losing mass.

theorem Anderson4D.prod_nx_sqrt_factorial_sub_le {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (S : NXClass → ℕ) (hsub : ∀ a ∈ nxCarrier Nm mu, S a ≤ multiplicityNX Nm mu a) : ∏ a ∈ nxCarrier Nm mu, √↑(multiplicityNX Nm mu a - S a).factorial ≤ √↑(totalMultiplicity mu - ∑ a ∈ nxCarrier Nm mu, S a).factorial

The deficit factorials from all active (N,X) fibers combine into the single global (m-s)! factor in (5.89).

theorem Anderson4D.prod_singleScaleFactorialEnvelope_le {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (S : NXClass → ℕ) (hsub : ∀ a ∈ nxCarrier Nm mu, S a ≤ multiplicityNX Nm mu a) : ∏ a ∈ nxCarrier Nm mu, singleScaleFactorialEnvelope a.2 (singleScaleSigma2 Nm mu a).2 (multiplicityNX Nm mu a) (S a) ≤ (2 * Real.exp 1) ^ totalMultiplicity mu * √↑(totalMultiplicity mu - ∑ a ∈ nxCarrier Nm mu, S a).factorial * ∏ l : HeppLeaf t, √↑(leafMultiplicity mu l).factorial

Multiplying the per-fiber bounds gives precisely one exponential factor, one global deficit factorial, and one factorial for every original leaf. This is the complete numerical passage from the product following (5.88) to the factorial part of (5.89).

theorem Anderson4D.prod_singleScalePrintedFiberFactor_le {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (S : NXClass → ℕ) (hsub : ∀ a ∈ nxCarrier Nm mu, S a ≤ multiplicityNX Nm mu a) : ∏ a ∈ nxCarrier Nm mu, singleScalePrintedFiberFactor a.2 (singleScaleSigma2 Nm mu a).2 (multiplicityNX Nm mu a) (S a) ≤ (2 * Real.exp 1) ^ totalMultiplicity mu * √↑(totalMultiplicity mu - ∑ a ∈ nxCarrier Nm mu, S a).factorial * ∏ l : HeppLeaf t, √↑(leafMultiplicity mu l).factorial

Paper-facing form of the global factorial absorption: the left side is the literal product of (X √Y)^M (XY)^(-S/2) from the sentence after (5.88).

theorem Anderson4D.prod_singleScalePrintedFiberFactor_le_of_ledgers {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (S : NXClass → ℕ) (m s : ℕ) (hsub : ∀ a ∈ nxCarrier Nm mu, S a ≤ multiplicityNX Nm mu a) (hm : totalMultiplicity mu = m) (hs : ∑ a ∈ nxCarrier Nm mu, S a = s) : ∏ a ∈ nxCarrier Nm mu, singleScalePrintedFiberFactor a.2 (singleScaleSigma2 Nm mu a).2 (multiplicityNX Nm mu a) (S a) ≤ (2 * Real.exp 1) ^ m * √↑(m - s).factorial * ∏ l : HeppLeaf t, √↑(leafMultiplicity mu l).factorial

The same result with the global ledgers ∑ M_{N,X}=m and ∑ S_{N,X}=s rewritten exactly as they appear in (5.89).