Proposition 4.1 provider at the R-324 truncation

This module packages the proved truncation form of Proposition 4.1 as the literal-head provider consumed by the within-half R-324 iteration.

The only order comparison is the structural fact that every extracted block has order at most the ambient half-order. Thus the provider introduces no analytic assumption beyond the positivity, cutoff, and truncation hypotheses already present in proposition41_at_truncation.

theorem Anderson4D.exists_r324WithinHalfProp41Provider_at_truncation (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ), 0 < supportConstant ∧ 0 < C ∧ ∀ (lam ε : ℝ) (m : ℕ) (pairing : PartialPairing (Fin m)), 0 < lam → 0 < ε → ε ≤ 1 → m ≤ truncOrder ε → R324WithinHalfProp41Provider ρ C lam ε supportConstant pairing

Proposition 4.1 at the paper truncation supplies its estimates uniformly at every literal head of every within-half residual suffix.

The logarithmic lower bound used by the subsequent one-block collapse is deliberately absent here: it is not a hypothesis of Proposition 4.1.

Compatible budget and analytic traces

theorem Anderson4D.r324WithinHalfBudgetLocalBlockProvider_of_localBlockProvider {ρ : SmoothCutoff} {C lam ε K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (hA : 1 ≤ A) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K pairing) : R324WithinHalfBudgetLocalBlockProvider ρ C lam ε K A pairing

A local analytic block provider promotes to the complete budget update when the uniform outgoing Green scale is at least one.

This conversion keeps the same one-block constant K. It is the small compatibility fact needed to build the numerical and analytic terminal traces from one Proposition 4.1 closure theorem.

theorem Anderson4D.R324WithinHalfResidualPrefix.exists_r324FullPairingBudgetTerminalAdapter_at_truncation (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ) (K : ℝ) (A : ℝ), 0 < supportConstant ∧ 0 < C ∧ 0 < K ∧ 1 ≤ A ∧ ∀ (lam ε : ℝ) (q : ℕ) (κ : PartialPairing (Fin (2 * q))), 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → q ≤ truncOrder ε → 1 ≤ q → κ.IsFull → ∃ (budget : R324FullPairingBudgetStopTrace κ), Nonempty (R324FullPairingBudgetTerminalAdapter budget)

At the paper truncation, one choice of Proposition 4.1 constants and one one-block constant construct a compatible full-pairing budget stop and analytic terminal assembly.

The two traces start from the same uniform all-Green certificate and use the same local constant K. Their scale-update functions remain distinct, as required by the budget ledger; R324FullPairingBudgetTerminalAdapter identifies only their canonical residual state.