Complete edge-budget invariant for the R-324 within-half schedule

The analytic one-block estimate absorbs the predecessor and all internal head-edge scales. The outgoing head edge is a free Green factor, but its slot is deleted from the sparse carrier. This module inserts that one outgoing scale into a numerical budget update and proves the exact active product recurrence through the genuine suffix.

def Anderson4D.R324WithinHalfResidualPrefix.headBlockSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : Finset (Fin (m + 1))

All active edge slots deleted with the literal head: its standard internal slots and its outgoing right-endpoint slot.

Equations

• res.headBlockSlots head tail hremaining = res.headInternalSlots head tail hremaining ∪ {(Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot}

theorem Anderson4D.R324WithinHalfResidualPrefix.headBlockSlots_subset_activeEdgeSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : res.headBlockSlots head tail hremaining ⊆ res.activeEdgeSlots

theorem Anderson4D.R324WithinHalfResidualPrefix.predecessorSlot_not_mem_headBlockSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : r324WithinHalfPredecessorSlot res.state head ∉ res.headBlockSlots head tail hremaining

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_activeEdgeSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).activeEdgeSlots = res.activeEdgeSlots \ res.headBlockSlots head tail hremaining

Deleting one literal block removes exactly its internal and outgoing edge slots from the active scale carrier.

def Anderson4D.R324WithinHalfResidualPrefix.headBlockScaleProduct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ) : ℝ

Product of all numerical scales deleted with the head block.

Equations

• res.headBlockScaleProduct head tail hremaining scale = ∏ edge ∈ res.headBlockSlots head tail hremaining, scale edge

theorem Anderson4D.R324WithinHalfResidualPrefix.headBlockScaleProduct_eq_internal_mul_outgoing {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ) : res.headBlockScaleProduct head tail hremaining scale = r324WithinHalfInternalEdgeScaleProduct (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining) scale * scale (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot

The complete block budget is the analytic internal-edge product times the outgoing free-Green scale.

def Anderson4D.R324WithinHalfResidualPrefix.budgetUpdatedEdgeScale {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ) (C : ℝ) : ℝ → (K : ℝ) → Fin (m + 1) → ℝ

Numerical update which absorbs every deleted block scale, including the outgoing free-Green slot.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.budgetUpdatedEdgeScale_predecessor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ) (C lam✝ K : ℝ) : res.budgetUpdatedEdgeScale head tail hremaining scale C lam✝ K (r324WithinHalfPredecessorSlot res.state head) = scale (r324WithinHalfPredecessorSlot res.state head) * res.headBlockScaleProduct head tail hremaining scale * (C * lam✝) ^ (2 * residualBlockOrder head.2) * K

theorem Anderson4D.R324WithinHalfResidualPrefix.budgetUpdatedEdgeScale_of_ne {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ) (C lam✝ K : ℝ) (edge : Fin (m + 1)) (hne : edge ≠ r324WithinHalfPredecessorSlot res.state head) : res.budgetUpdatedEdgeScale head tail hremaining scale C lam✝ K edge = scale edge

theorem Anderson4D.R324WithinHalfResidualPrefix.budgetUpdatedEdgeScale_predecessor_eq_analytic_mul_outgoing {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ) (C lam✝ K : ℝ) : res.budgetUpdatedEdgeScale head tail hremaining scale C lam✝ K (r324WithinHalfPredecessorSlot res.state head) = r324WithinHalfUpdatedEdgeScale (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining) scale C lam✝ K (r324WithinHalfPredecessorSlot res.state head) * scale (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot

At the predecessor, the budget update is the analytic scale multiplied by the one outgoing scale.

theorem Anderson4D.R324WithinHalfResidualPrefix.activeEdgeScaleProduct_budgetUpdate {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ) (C lam✝ K : ℝ) : ∏ edge ∈ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).activeEdgeSlots, res.budgetUpdatedEdgeScale head tail hremaining scale C lam✝ K edge = (∏ edge ∈ res.activeEdgeSlots, scale edge) * (C * lam✝) ^ (2 * residualBlockOrder head.2) * K

Exact active scale-product recurrence for one budget update.

Certificate enlargement

theorem Anderson4D.R324WithinHalfEdgeCertificate.of_pointwise_scale_le {m : ℕ} {state : R324WithinHalfEdgeState m} {scale budget : Fin (m + 1) → ℝ} (hcert : R324WithinHalfEdgeCertificate state scale) (hle : ∀ (edge : Fin (m + 1)), scale edge ≤ budget edge) : R324WithinHalfEdgeCertificate state budget

Uniform initial normalization

theorem Anderson4D.exists_r324InitialWithinHalfEdgeCertificate_one_le_uniform : ∃ (A : ℝ), 1 ≤ A ∧ ∀ (m : ℕ), R324WithinHalfEdgeCertificate (r324InitialWithinHalfEdgeState m) fun (x : Fin (m + 1)) => A

A single scale at least one controls every all-Green initial state, uniformly in the ambient perturbative order.

Reachable budget histories

inductive Anderson4D.R324WithinHalfBudgetScaleReachable {m : ℕ} (pairing : PartialPairing (Fin m)) (ρ : SmoothCutoff) (C lam ε K A : ℝ) : R324WithinHalfEdgeState m → (Fin (m + 1) → ℝ) → Prop

Quantitative budget reachability follows the same literal schedule heads as the analytic residual prefix.

• initial {m : ℕ} {pairing : PartialPairing (Fin m)} {ρ : SmoothCutoff} {C lam ε K A : ℝ} : R324WithinHalfBudgetScaleReachable pairing ρ C lam ε K A (r324InitialWithinHalfEdgeState m) fun (x : Fin (m + 1)) => A
• afterHead {m : ℕ} {pairing : PartialPairing (Fin m)} {ρ : SmoothCutoff} {C lam ε K A : ℝ} {scale : Fin (m + 1) → ℝ} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (previous : R324WithinHalfBudgetScaleReachable pairing ρ C lam ε K A res.state scale) : R324WithinHalfBudgetScaleReachable pairing ρ C lam ε K A (res.afterHead head tail hremaining).state (res.budgetUpdatedEdgeScale head tail hremaining scale C lam K)

theorem Anderson4D.R324WithinHalfBudgetScaleReachable.edgeScale_eq_base_of_processed_right_lt {ρ : SmoothCutoff} {C lam ε K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {state : R324WithinHalfEdgeState m} {scale : Fin (m + 1) → ℝ} (hreach : R324WithinHalfBudgetScaleReachable pairing ρ C lam ε K A state scale) (edge : Fin (m + 1)) (hfuture : ∀ earlier ∈ state.processed, ↑earlier.1.2 < ↑edge) : scale edge = A

Every future edge scale is still the initial Green budget.

theorem Anderson4D.R324WithinHalfBudgetScaleReachable.outgoingScale_eq_base {ρ : SmoothCutoff} {C lam ε K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {state : R324WithinHalfEdgeState m} {scale : Fin (m + 1) → ℝ} (hreach : R324WithinHalfBudgetScaleReachable pairing ρ C lam ε K A state scale) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hstate : res.state = state) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : scale (res.headContext head tail hremaining).outgoingSlot = A

The outgoing budget scale of the current literal head is exactly the initial Green budget.

theorem Anderson4D.R324WithinHalfBudgetScaleReachable.promote_afterHead_certificate {ρ : SmoothCutoff} {C lam ε K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {state : R324WithinHalfEdgeState m} {scale : Fin (m + 1) → ℝ} (hreach : R324WithinHalfBudgetScaleReachable pairing ρ C lam ε K A state scale) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hstate : res.state = state) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hA : 1 ≤ A) (rawCertificate : R324WithinHalfEdgeCertificate (res.afterHead head tail hremaining).state (r324WithinHalfUpdatedEdgeScale (res.headContext head tail hremaining) scale C lam K)) : R324WithinHalfEdgeCertificate (res.afterHead head tail hremaining).state (res.budgetUpdatedEdgeScale head tail hremaining scale C lam K)

The analytic one-block certificate promotes to the complete numerical budget update once the unchanged outgoing Green scale is at least one.

Exact active-product ledger

def Anderson4D.r324WithinHalfProcessedOrder {m : ℕ} (state : R324WithinHalfEdgeState m) : ℕ

Total perturbative order absorbed into a within-half edge state.

Equations

• Anderson4D.r324WithinHalfProcessedOrder state = (List.map (fun (step : Anderson4D.R322ExtractionStep m) => Anderson4D.residualBlockOrder step.2) state.processed).sum

theorem Anderson4D.R324WithinHalfBudgetScaleReachable.activeEdgeScaleProduct_eq {ρ : SmoothCutoff} {C lam ε K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {state : R324WithinHalfEdgeState m} {scale : Fin (m + 1) → ℝ} (hreach : R324WithinHalfBudgetScaleReachable pairing ρ C lam ε K A state scale) : ∏ edge ∈ {0} ∪ Finset.image r324InternalVertexEdgeSlot state.active, scale edge = (∏ _edge ∈ {0} ∪ Finset.image r324InternalVertexEdgeSlot (r324InitialWithinHalfEdgeState m).active, A) * (C * lam) ^ (2 * r324WithinHalfProcessedOrder state) * K ^ state.processed.length

Every budget-reachable history satisfies the exact active-scale product recurrence. The initial active product is intentionally left literal here; its uniform numerical absorption is a separate step.

Budget-certified local closure and literal suffix iteration

def Anderson4D.R324WithinHalfBudgetLocalBlockProvider (ρ : SmoothCutoff) (C lam ε K A : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) : Prop

A one-block provider for the complete numerical budget. Besides the actual local predecessor inequality, it transports both reachability and the slotwise edge certificate to the literal suffix.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.exists_r324WithinHalf_budgetLocalBlockProvider {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (ρ : SmoothCutoff) (C lam ε A : ℝ) (m : ℕ) (pairing : PartialPairing (Fin m)), 1 ≤ A → 0 < C → 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → R324WithinHalfProp41Provider ρ C lam ε supportConstant pairing → R324WithinHalfBudgetLocalBlockProvider ρ C lam ε K A pairing

Proposition 4.1 supplies a genuine complete-budget provider at every literal within-half head.

theorem Anderson4D.exists_r324WithinHalf_terminalBudgetCertificate_of_provider {ρ : SmoothCutoff} {C lam ε K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (provider : R324WithinHalfBudgetLocalBlockProvider ρ C lam ε K A pairing) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ) (reachable : R324WithinHalfBudgetScaleReachable pairing ρ C lam ε K A res.state scale) (certificate : R324WithinHalfEdgeCertificate res.state scale) : ∃ (terminal : R324WithinHalfResidualPrefix ρ lam ε pairing) (terminalScale : Fin (m + 1) → ℝ), terminal.remaining = [] ∧ terminal.state.processed = r322AnalyticSchedule pairing ∧ R324WithinHalfBudgetScaleReachable pairing ρ C lam ε K A terminal.state terminalScale ∧ R324WithinHalfEdgeCertificate terminal.state terminalScale

Structural recursion through the literal remaining suffix reaches an empty residual prefix while retaining the complete quantitative budget.

theorem Anderson4D.exists_r324WithinHalf_uniformTerminalBudget_of_prop41 {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∃ (A : ℝ), 1 ≤ A ∧ ∀ (ρ : SmoothCutoff) (C lam ε : ℝ) (m : ℕ) (pairing : PartialPairing (Fin m)), 0 < C → 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → R324WithinHalfProp41Provider ρ C lam ε supportConstant pairing → ∃ (terminal : R324WithinHalfResidualPrefix ρ lam ε pairing) (terminalScale : Fin (m + 1) → ℝ), terminal.remaining = [] ∧ terminal.state.processed = r322AnalyticSchedule pairing ∧ R324WithinHalfBudgetScaleReachable pairing ρ C lam ε K A terminal.state terminalScale ∧ R324WithinHalfEdgeCertificate terminal.state terminalScale

Uniform within-half terminal budget obtained by iterating the actual Proposition 4.1 block estimate from the all-Green initial state. Both numerical constants are chosen before the order and pairing.