The carrier-relative terminal collapse for R-322

After every proper schedule step has been integrated, the last extraction block occupies the whole remaining carrier. This module reads its current heterogeneous edges in increasing carrier order and identifies the signed terminal spatial integral with the genuine Proposition 4.1 primitive kernel.

structure Anderson4D.R322AnalyticTerminalStepContext (q : ℕ) (hq : 1 ≤ q) : Type

Certified data at the terminal step of a non-splitting R-322 schedule.

• state : R322AnalyticEdgeState q hq
• pairing : PartialPairing (Fin (2 * q))
• pairing_mem : self.pairing ∈ nonSplitPairings q
• terminal : R322ExtractionStep (2 * q)
• schedule_eq : r322AnalyticSchedule self.pairing = self.state.processed ++ [self.terminal]
• terminal_endpoint : self.terminal.1 = r322WholeEndpoint q hq

theorem Anderson4D.R322AnalyticTerminalStepContext.terminal_mem_schedule {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) : ctx.terminal ∈ r322AnalyticSchedule ctx.pairing

theorem Anderson4D.R322AnalyticTerminalStepContext.block_mem_extractionBlocks {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) : ctx.terminal.2 ∈ extractionBlocks ctx.pairing

theorem Anderson4D.R322AnalyticTerminalStepContext.blockFullyPaired {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) : IsFullyPairedOn ctx.pairing ctx.terminal.2

theorem Anderson4D.R322AnalyticTerminalStepContext.one_le_blockOrder {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) : 1 ≤ residualBlockOrder ctx.terminal.2

theorem Anderson4D.R322AnalyticTerminalStepContext.block_eq_active {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) : ctx.terminal.2 = ctx.state.active

The terminal concrete block is precisely the current active carrier.

def Anderson4D.R322AnalyticTerminalStepContext.blockOrderIso {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) : Fin (2 * residualBlockOrder ctx.terminal.2) ≃o ↥ctx.terminal.2

Increasing enumeration of the residual terminal carrier.

Equations

• ctx.blockOrderIso = Anderson4D.residualPrimitiveBlockOrderIso ctx.pairing ctx.terminal.2 ⋯

theorem Anderson4D.R322AnalyticTerminalStepContext.blockOrderIso_last {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) : ↑(ctx.blockOrderIso (primitiveLast (residualBlockOrder ctx.terminal.2) ⋯)) = ⟨2 * q - 1, ⋯⟩

The last point in the increasing terminal-block enumeration is the global right endpoint.

def Anderson4D.R322AnalyticTerminalStepContext.internalEdge {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) (j : Fin (2 * residualBlockOrder ctx.terminal.2 - 1)) : Fin (2 * q - 1)

Ambient edge slot at the jth internal adjacency of the terminal carrier.

Equations

• ctx.internalEdge j = ⟨↑↑(ctx.blockOrderIso ⟨↑j, ⋯⟩), ⋯⟩

def Anderson4D.R322AnalyticTerminalStepContext.internalEdges {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) : Fin (2 * residualBlockOrder ctx.terminal.2 - 1) → T4 → ℝ

The current heterogeneous edge family, read in the increasing order of the terminal carrier. Previously collapsed nonlocal kernels therefore occupy exactly the slots at which they survived.

Equations

• ctx.internalEdges j = ctx.state.edges (ctx.internalEdge j)

noncomputable def Anderson4D.R322AnalyticTerminalStepContext.terminalSpatialIntegral {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) (ρ : SmoothCutoff) (lam ε : ℝ) (z w : T4) : ℝ

Signed spatial integral of the remaining whole carrier.

Equations

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

theorem Anderson4D.R322AnalyticTerminalStepContext.terminalSpatialIntegral_eq_primitiveKernel {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticTerminalStepContext q hq) (ρ : SmoothCutoff) (lam ε : ℝ) (z w : T4) (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 w u)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.terminal.2 - 2)) => paperMeasure)) : ctx.terminalSpatialIntegral ρ lam ε z w = primitiveKernel ρ lam ε (residualBlockOrder ctx.terminal.2) ⋯ ctx.internalEdges z w

The terminal signed integral is exactly the heterogeneous primitive kernel to which Proposition 4.1 applies.