The active-edge ledger at the R-322 terminal step

At the terminal step, the concrete block is the entire remaining carrier. Consequently its canonically ordered internal chain slots are exactly the ambient edge slots whose left vertex is still active. This module proves that finite-set identity and the resulting exact scale-product identity.

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

Ambient image of the terminal primitive kernel's internal edge slots.

Equations

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

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

theorem Anderson4D.R322AnalyticTerminalStepContext.internalEdgesFinset_subset_activeEdges {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) : ctx.internalEdgesFinset ⊆ r322AnalyticActiveEdges ctx.state

theorem Anderson4D.R322AnalyticTerminalStepContext.activeEdges_subset_internalEdgesFinset {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) : r322AnalyticActiveEdges ctx.state ⊆ ctx.internalEdgesFinset

Every active ambient edge occurs at a unique internal slot of the terminal primitive block.

theorem Anderson4D.R322AnalyticTerminalStepContext.internalEdgesFinset_eq_activeEdges {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) : ctx.internalEdgesFinset = r322AnalyticActiveEdges ctx.state

The terminal internal slots are exactly the still-active ambient edge slots.

theorem Anderson4D.R322AnalyticTerminalStepContext.internalEdgeScaleProduct_eq_activeEdgeScaleProduct {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) (scale : Fin (2 * q - 1) → ℝ) : ∏ j : Fin (2 * residualBlockOrder ctx.terminal.2 - 1), scale (ctx.internalEdge j) = ∏ edge ∈ r322AnalyticActiveEdges ctx.state, scale edge

The scale product seen by the final Proposition 4.1 kernel is exactly the active-edge scale product carried through the proper-prefix induction.

theorem Anderson4D.R322AnalyticTerminalStepContext.abs_terminalSpatialIntegral_le_activeEdgeScaleProduct_mul_majorant {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) (ρ : SmoothCutoff) (lam ε primitiveConstant supportConstant : ℝ) (scale : Fin (2 * q - 1) → ℝ) (hcert : R322AnalyticEdgeCertificate ctx.state scale) (hprop : ∀ (H : Fin (2 * residualBlockOrder ctx.terminal.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder ctx.terminal.2) H → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.terminal.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε (residualBlockOrder ctx.terminal.2) ⋯ H) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder ctx.terminal.2) ⋯ H supportConstant primitiveConstant) (z : T4) (hz : z ≠ 0) (hint : ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.terminal.2))), MeasureTheory.Integrable (fun (u : Fin (2 * residualBlockOrder ctx.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.terminal.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.terminal.2) ⋯ z 0 u)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.terminal.2 - 2)) => paperMeasure)) : |ctx.terminalSpatialIntegral ρ lam ε z 0| ≤ (∏ edge ∈ r322AnalyticActiveEdges ctx.state, scale edge) * primitiveKernelMajorant primitiveConstant lam ε supportConstant (residualBlockOrder ctx.terminal.2) z

Proposition 4.1 at the terminal carrier, with the exact active-edge product furnished by the proper-prefix budget ledger.