Closing the two certified within-half scale ledgers

This file contains only the finite combinatorial bookkeeping needed to use the compatible analytic budgets. It identifies the all-Green initial scale product, bounds the number of processed blocks by their total perturbative order, and combines the two terminal scale products with the initial nested cross order.

theorem Anderson4D.r324InitialActiveScaleProduct_eq_pow (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (A : ℝ) : ∏ _edge ∈ {0} ∪ Finset.image r324InternalVertexEdgeSlot (r324InitialWithinHalfEdgeState m).active, A = A ^ (m + 1)

The literal all-Green active scale product has one factor for each of the m + 1 production-edge slots.

theorem Anderson4D.r322AnalyticSchedule_length_le_orderSum {m : ℕ} (pairing : PartialPairing (Fin m)) : (r322AnalyticSchedule pairing).length ≤ (List.map (fun (step : R322ExtractionStep m) => residualBlockOrder step.2) (r322AnalyticSchedule pairing)).sum

Every block in the analytic schedule has positive perturbative order, so the schedule length is no larger than its order sum.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminal_processedOrder_eq_initialRemainingOrder {ρ : SmoothCutoff} {lam ε A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (trace : (initial ρ lam ε pairing).R324WithinHalfCertifiedAnalyticTrace fun (x : Fin (m + 1)) => A) : r324WithinHalfProcessedOrder trace.terminalPrefix.state = (initial ρ lam ε pairing).remainingOrder

A complete certified trace has processed exactly the order of the initial analytic suffix.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminal_processedLength_le_initialRemainingOrder {ρ : SmoothCutoff} {lam ε A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (trace : (initial ρ lam ε pairing).R324WithinHalfCertifiedAnalyticTrace fun (x : Fin (m + 1)) => A) : trace.terminalPrefix.state.processed.length ≤ (initial ρ lam ε pairing).remainingOrder

The number of processed blocks in a complete certified trace is no larger than the initial suffix order.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324CompatibleAnalyticBudgetTrace.initial_analytic_activeEdgeScaleProduct_le_closedForm {ρ : SmoothCutoff} {C lam ε K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (data : (initial ρ lam ε pairing).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A) : ∏ edge ∈ data.analytic.terminalPrefix.activeEdgeSlots, data.analytic.terminalScale edge ≤ A ^ (m + 1) * (C * lam) ^ (2 * (initial ρ lam ε pairing).remainingOrder) * K ^ data.analytic.terminalPrefix.state.processed.length

Closed form of one terminal scale product when its certified budget starts from the constant all-Green scale.

theorem Anderson4D.r324_twoHalf_initial_terminalScale_mul_majorant_le {ρ : SmoothCutoff} {C K A B lam ε supportConstant : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} (hA : 0 ≤ A) (hC : 0 ≤ C) (hK : 0 ≤ K) (hB : 0 ≤ B) (hlam : 0 ≤ lam) (leftData : (R324WithinHalfResidualPrefix.initial ρ lam ε κp).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A) (rightData : (R324WithinHalfResidualPrefix.initial ρ lam ε κm).R324CompatibleAnalyticBudgetTrace fun (x : Fin (m + 1)) => A) (π : ↥κp.singles ≃ ↥κm.singles) (hm : 1 ≤ m) (z : T4) : ((∏ edge ∈ leftData.analytic.terminalPrefix.activeEdgeSlots, leftData.analytic.terminalScale edge) * ∏ edge ∈ rightData.analytic.terminalPrefix.activeEdgeSlots, rightData.analytic.terminalScale edge) * invSqKerMass ^ 4 * primitiveInsertedMajorant B lam ε supportConstant (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder z ≤ primitiveInsertedMajorant (r324TwoHalfCompleteAbsorbedBase A C K B) lam ε supportConstant m z

The two certified terminal scale products and the complete initial nested-cross inserted majorant are absorbed into one ambient-order inserted majorant. This is the exact three-schedule order ledger used after the endpoint/run integral estimate.