Absorbing the complete nested-cross order ledger

The proper shells contribute (D λ)^(2p) and the final complete block contributes one paper-volume factor times the order-t inserted majorant. This file absorbs both into one order-p+t inserted majorant with a single named base constant. The proof is purely numerical and does not change the order in which any physical integral or finite pairing sum is evaluated.

noncomputable def Anderson4D.r324CompleteAbsorbedBase (D C : ℝ) : ℝ

A convenient base large enough to absorb both head constants and the single translation-volume cost.

Equations

• Anderson4D.r324CompleteAbsorbedBase D C = max 1 D * max 1 C * max 1 ((2 * Real.pi) ^ Anderson4D.dim)

theorem Anderson4D.r324CompleteAbsorbedBase_pos (D C : ℝ) : 0 < r324CompleteAbsorbedBase D C

theorem Anderson4D.r324_complete_prefix_mul_terminalMajorant_le {D C lam ε supportConstant : ℝ} (hD : 0 ≤ D) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (p t : ℕ) (htotal : 1 ≤ p + t) (z : T4) : (D * lam) ^ (2 * p) * (2 * Real.pi) ^ dim * primitiveInsertedMajorant C lam ε supportConstant t z ≤ primitiveInsertedMajorant (r324CompleteAbsorbedBase D C) lam ε supportConstant (p + t) z

Proper-prefix cost times the final order-t majorant is pointwise dominated by the single majorant at the total order.

theorem Anderson4D.r324_complete_prefix_mul_terminalIntegral_le {D C lam ε supportConstant : ℝ} (hD : 0 ≤ D) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hε : 0 < ε) (p t : ℕ) (htotal : 1 ≤ p + t) : (D * lam) ^ (2 * p) * ((2 * Real.pi) ^ dim * ∫ (z : T4), primitiveInsertedMajorant C lam ε supportConstant t z ∂paperMeasure) ≤ ∫ (z : T4), primitiveInsertedMajorant (r324CompleteAbsorbedBase D C) lam ε supportConstant (p + t) z ∂paperMeasure

Integrated form used by the complete nested budget iterator.