Quantitative reachability along the genuine R-322 proper prefix

The qualitative sparse-carrier history and its numerical edge budget are advanced together. At each proper step the primitive certificate is built from Proposition 4.1 and the current edge certificate; in particular, its fixed-endpoint integrability field is proved before the one-block estimate is applied. The analytic output is then enlarged to the complete deleted-block budget using the invariant value of the future outgoing Green scale.

structure Anderson4D.R322AnalyticQuantitativePrefixData {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (C lam ε K A : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (pre : List (R322ExtractionStep (2 * q))) : Type

Complete qualitative and quantitative data carried by one genuine proper prefix of the production R-322 schedule.

• state : R322AnalyticEdgeState q hq
• scale : Fin (2 * q - 1) → ℝ
• absorbed : R322AnalyticAbsorbedState ρ lam ε hq κ hκ self.state
• processed : self.state.processed = pre
• budgetReachable : R322AnalyticBudgetScaleReachable hq ρ C lam ε K A κ hκ self.state self.scale
• edgeCertificate : R322AnalyticEdgeCertificate self.state self.scale

theorem Anderson4D.exists_r322AnalyticQuantitativePrefixData (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ) (K : ℝ) (A : ℝ), 0 < supportConstant ∧ 0 < C ∧ 0 < K ∧ 1 ≤ A ∧ (∀ (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), 0 < lam → 0 < ε → ε ≤ 1 → n ≤ truncOrder ε → IsAdmissiblePrimitiveInput n G → MemEClassT4 (primitiveKernelDiff ρ lam ε n hn G) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε n hn G) ∧ PrimitiveKernelBounds ρ lam ε n hn G supportConstant C) ∧ ∀ (lam ε : ℝ) (q : ℕ) (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (pre suffix : List (R322ExtractionStep (2 * q))), 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → q ≤ truncOrder ε → r322AnalyticSchedule κ = pre ++ suffix → (∀ step ∈ pre, step.1 ≠ r322WholeEndpoint q hq) → Nonempty (R322AnalyticQuantitativePrefixData hq ρ C lam ε K A κ hκ pre)

Proposition 4.1 and the one-block theorem provide constants, chosen before the coupling, mollification scale, perturbative order, pairing, and proper prefix, for which every genuine proper prefix has a simultaneous absorbed-state, budget-reachability, and slotwise edge certificate.

The initial Green scale is chosen once for every perturbative order and is normalized by 1 ≤ A. Thus A, the Proposition 4.1 constant C, and the one-block constant K are all uniform over q and the whole prefix.