Active-edge product ledger for the R-322 analytic schedule

The quantitative R-322 induction controls only edges whose left vertex is still present in the sparse carrier. This module packages that finite set and proves its exact behavior under one proper block deletion.

def Anderson4D.r322AnalyticActiveEdges {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) : Finset (Fin (2 * q - 1))

Ambient edge slots whose left vertex remains in the sparse carrier.

Equations

• Anderson4D.r322AnalyticActiveEdges state = {edge : Fin (2 * q - 1) | Anderson4D.r322AnalyticEdgeLeftVertex edge ∈ state.active}

@[simp]

theorem Anderson4D.mem_r322AnalyticActiveEdges {q : ℕ} {hq : 1 ≤ q} {state : R322AnalyticEdgeState q hq} {edge : Fin (2 * q - 1)} : edge ∈ r322AnalyticActiveEdges state ↔ r322AnalyticEdgeLeftVertex edge ∈ state.active

def Anderson4D.R322AnalyticProperStepContext.blockEdge {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (i : ↥ctx.step.2) : Fin (2 * q - 1)

Every vertex of a proper concrete block determines an ambient edge slot: the proper-block bound excludes the global last vertex.

Equations

• ctx.blockEdge i = ⟨↑↑i, ⋯⟩

def Anderson4D.R322AnalyticProperStepContext.blockEdges {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : Finset (Fin (2 * q - 1))

Edge slots removed together with the proper concrete block.

Equations

• ctx.blockEdges = Finset.image ctx.blockEdge ctx.step.2.attach

theorem Anderson4D.R322AnalyticProperStepContext.blockEdge_injective {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : Function.Injective ctx.blockEdge

@[simp]

theorem Anderson4D.R322AnalyticProperStepContext.mem_blockEdges_iff {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) {edge : Fin (2 * q - 1)} : edge ∈ ctx.blockEdges ↔ r322AnalyticEdgeLeftVertex edge ∈ ctx.step.2

theorem Anderson4D.R322AnalyticProperStepContext.blockEdges_subset_activeEdges {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.blockEdges ⊆ r322AnalyticActiveEdges ctx.state

theorem Anderson4D.R322AnalyticProperStepContext.predecessorEdge_mem_activeEdges {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.predecessorEdge ∈ r322AnalyticActiveEdges ctx.state

theorem Anderson4D.R322AnalyticProperStepContext.predecessorEdge_not_mem_blockEdges {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.predecessorEdge ∉ ctx.blockEdges

theorem Anderson4D.R322AnalyticProperStepContext.blockOrderIso_last {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ↑(ctx.blockOrderIso (primitiveLast (residualBlockOrder ctx.step.2) ⋯)) = ctx.step.1.2

The last point in the canonical increasing block enumeration is the selected right endpoint.

def Anderson4D.R322AnalyticProperStepContext.internalEdgesFinset {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : Finset (Fin (2 * q - 1))

Ambient slots of the internal chain edges in standard block order.

Equations

• ctx.internalEdgesFinset = Finset.image ctx.internalEdge Finset.univ

theorem Anderson4D.R322AnalyticProperStepContext.internalEdge_injective {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : Function.Injective ctx.internalEdge

theorem Anderson4D.R322AnalyticProperStepContext.internalEdgesFinset_subset_blockEdges {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.internalEdgesFinset ⊆ ctx.blockEdges

theorem Anderson4D.R322AnalyticProperStepContext.outgoingEdge_mem_blockEdges {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.outgoingEdge ∈ ctx.blockEdges

theorem Anderson4D.R322AnalyticProperStepContext.outgoingEdge_not_mem_internalEdgesFinset {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.outgoingEdge ∉ ctx.internalEdgesFinset

theorem Anderson4D.R322AnalyticProperStepContext.card_blockEdges {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.blockEdges.card = 2 * residualBlockOrder ctx.step.2

theorem Anderson4D.R322AnalyticProperStepContext.card_internalEdgesFinset {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.internalEdgesFinset.card = 2 * residualBlockOrder ctx.step.2 - 1

theorem Anderson4D.R322AnalyticProperStepContext.internalEdgesFinset_union_outgoing {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.internalEdgesFinset ∪ {ctx.outgoingEdge} = ctx.blockEdges

The deleted block slots split into its internal chain slots and its outgoing right-endpoint slot.

theorem Anderson4D.R322AnalyticProperStepContext.activeEdges_nextState {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (lam ε : ℝ) : r322AnalyticActiveEdges (ctx.nextState ρ lam ε) = r322AnalyticActiveEdges ctx.state \ ctx.blockEdges

One proper state update removes exactly the edge slots based at the vertices of its concrete block.

Exact product update on the active carrier

def Anderson4D.R322AnalyticProperStepContext.activeEdgeScaleProduct {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) : ℝ

Product of the numerical edge scales which remain visible on a sparse carrier.

Equations

• ctx.activeEdgeScaleProduct scale = ∏ edge ∈ Anderson4D.r322AnalyticActiveEdges ctx.state, scale edge

def Anderson4D.R322AnalyticProperStepContext.blockEdgeScaleProduct {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) : ℝ

Product of the scales based at the vertices deleted by this block.

Equations

• ctx.blockEdgeScaleProduct scale = ∏ edge ∈ ctx.blockEdges, scale edge

theorem Anderson4D.R322AnalyticProperStepContext.internalEdgesFinset_scaleProduct {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) : ∏ edge ∈ ctx.internalEdgesFinset, scale edge = r322AnalyticInternalEdgeScaleProduct ctx scale

The concrete internal-edge image has exactly the primitive certificate's heterogeneous scale product.

theorem Anderson4D.R322AnalyticProperStepContext.blockEdgeScaleProduct_eq_internal_mul_outgoing {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) : ctx.blockEdgeScaleProduct scale = r322AnalyticInternalEdgeScaleProduct ctx scale * scale ctx.outgoingEdge

The complete deleted-block budget is the actual primitive internal product times the one outgoing scale which the analytic collapse leaves as a free Green factor.

def Anderson4D.R322AnalyticProperStepContext.budgetUpdatedEdgeScale {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) (C lam K : ℝ) : Fin (2 * q - 1) → ℝ

Budget-level update which also absorbs the outgoing block-edge scale. The analytic update absorbs all other block edges; the outgoing free Green factor is inserted here only in the numerical majorant.

Equations

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

@[simp]

theorem Anderson4D.R322AnalyticProperStepContext.budgetUpdatedEdgeScale_predecessor {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) (C lam K : ℝ) : ctx.budgetUpdatedEdgeScale scale C lam K ctx.predecessorEdge = scale ctx.predecessorEdge * ctx.blockEdgeScaleProduct scale * (C * lam) ^ (2 * residualBlockOrder ctx.step.2) * K

theorem Anderson4D.R322AnalyticProperStepContext.budgetUpdatedEdgeScale_of_ne {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) (C lam K : ℝ) (edge : Fin (2 * q - 1)) (hne : edge ≠ ctx.predecessorEdge) : ctx.budgetUpdatedEdgeScale scale C lam K edge = scale edge

theorem Anderson4D.R322AnalyticProperStepContext.budgetUpdatedEdgeScale_predecessor_eq_actual_mul_outgoing {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) (C lam K : ℝ) : ctx.budgetUpdatedEdgeScale scale C lam K ctx.predecessorEdge = r322AnalyticUpdatedEdgeScale ctx scale (r322AnalyticInternalEdgeScaleProduct ctx scale) C lam K ctx.predecessorEdge * scale ctx.outgoingEdge

At the updated predecessor the budget scale is exactly the proved analytic scale times the outgoing scale; this is an identity, not an estimate.

theorem Anderson4D.R322AnalyticProperStepContext.activeEdgeScaleProduct_budgetUpdate {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε C lam K : ℝ) (scale : Fin (2 * q - 1) → ℝ) : ∏ edge ∈ r322AnalyticActiveEdges (ctx.nextState ρ lam ε), ctx.budgetUpdatedEdgeScale scale C lam K edge = ctx.activeEdgeScaleProduct scale * (C * lam) ^ (2 * residualBlockOrder ctx.step.2) * K

Because a proper block is a subset of the current carrier and its predecessor lies outside it, absorbing the complete block product at that predecessor preserves the old active product up to exactly the one new analytic factor.

theorem Anderson4D.R322AnalyticProperStepContext.edgeCertificate_of_pointwise_scale_le {q : ℕ} {hq : 1 ≤ q} {state : R322AnalyticEdgeState q hq} {scale budget : Fin (2 * q - 1) → ℝ} (hcert : R322AnalyticEdgeCertificate state scale) (hle : ∀ (edge : Fin (2 * q - 1)), scale edge ≤ budget edge) : R322AnalyticEdgeCertificate state budget

A slotwise edge certificate may be enlarged along a pointwise scale majorization.

theorem Anderson4D.R322AnalyticProperStepContext.edgeCertificate_to_budgetUpdatedEdgeScale {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (lam ε C K : ℝ) (scale : Fin (2 * q - 1) → ℝ) (hcert : R322AnalyticEdgeCertificate (ctx.nextState ρ lam ε) (r322AnalyticUpdatedEdgeScale ctx scale (r322AnalyticInternalEdgeScaleProduct ctx scale) C lam K)) (hout : 1 ≤ scale ctx.outgoingEdge) : R322AnalyticEdgeCertificate (ctx.nextState ρ lam ε) (ctx.budgetUpdatedEdgeScale scale C lam K)

Honest promotion from the scale delivered by the analytic one-block estimate to the complete deleted-block budget. The only extra numerical premise is the explicit outgoing-scale normalization 1 ≤ scale outgoing; without it the enlarged-budget conclusion is false in general.