Absorbing the two within-half scale ledgers and the complete cross run

This file is purely numerical. It combines the two literal Phase-A scale products with an inserted majorant at the remaining nested-cross order and uses the exact three-schedule order identity to obtain one inserted majorant at the ambient order.

noncomputable def Anderson4D.r324TwoHalfCompleteAbsorbedBase (A C K B : ℝ) : ℝ

One explicit base large enough to absorb the two all-Green initial scale products, the two Phase-A block costs, the complete nested-run base, and the four endpoint inverse-square masses.

Equations

• Anderson4D.r324TwoHalfCompleteAbsorbedBase A C K B = max 1 A ^ 2 * max 1 C * max 1 K * max 1 B * max 1 Anderson4D.invSqKerMass ^ 2

theorem Anderson4D.r324TwoHalfCompleteAbsorbedBase_pos (A C K B : ℝ) : 0 < r324TwoHalfCompleteAbsorbedBase A C K B

theorem Anderson4D.r324_twoHalf_complete_majorant_le {A C K B lam ε supportConstant : ℝ} (hA : 0 ≤ A) (hC : 0 ≤ C) (hK : 0 ≤ K) (hB : 0 ≤ B) (hlam : 0 ≤ lam) {m pleft pright cross leftLength rightLength : ℕ} (hm : 1 ≤ m) (horder : pleft + pright + cross = m) (hleftLength : leftLength ≤ pleft) (hrightLength : rightLength ≤ pright) (z : T4) : A ^ (m + 1) * (C * lam) ^ (2 * pleft) * K ^ leftLength * (A ^ (m + 1) * (C * lam) ^ (2 * pright) * K ^ rightLength) * invSqKerMass ^ 4 * primitiveInsertedMajorant B lam ε supportConstant cross z ≤ primitiveInsertedMajorant (r324TwoHalfCompleteAbsorbedBase A C K B) lam ε supportConstant m z

Pointwise inserted-majorant form of the preceding coefficient ledger.