One carrier-relative proper collapse for R-322

The standard block coordinates are read from the next concrete block in the sparse active carrier. Every chain kernel is taken from the current heterogeneous edge state, and the signed spatial integral is identified with the predecessor edge of the updated state.

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

Certified data for one proper step of the current schedule suffix.

• state : R322AnalyticEdgeState q hq
• pairing : PartialPairing (Fin (2 * q))
• pairing_mem : self.pairing ∈ nonSplitPairings q
• suffix : List (R322ExtractionStep (2 * q))
• step : R322ExtractionStep (2 * q)
• schedule_eq : r322AnalyticSchedule self.pairing = self.state.processed ++ self.step :: self.suffix
• proper : self.step.1 ≠ r322WholeEndpoint q hq

theorem Anderson4D.R322AnalyticProperStepContext.bounds {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : 0 < ↑ctx.step.1.1 ∧ ↑ctx.step.1.2 < 2 * q - 1

theorem Anderson4D.R322AnalyticProperStepContext.step_mem_schedule {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.step ∈ r322AnalyticSchedule ctx.pairing

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

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

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

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

Increasing enumeration of the current sparse concrete block.

Equations

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

theorem Anderson4D.R322AnalyticProperStepContext.blockVertex_bounds {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (i : Fin (2 * q)) (hi : i ∈ ctx.step.2) : 0 < ↑i ∧ ↑i < 2 * q - 1

def Anderson4D.R322AnalyticProperStepContext.internalLeftVertex {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (j : Fin (2 * residualBlockOrder ctx.step.2 - 1)) : Fin (2 * q)

Ambient vertex at the left of the jth internal active edge.

Equations

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

theorem Anderson4D.R322AnalyticProperStepContext.internalLeftVertex_mem_active {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (j : Fin (2 * residualBlockOrder ctx.step.2 - 1)) : ctx.internalLeftVertex j ∈ ctx.state.active

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

Ambient edge slot at the jth internal active adjacency.

Equations

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

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

The primitive block sees the current heterogeneous internal edges.

Equations

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

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

Equations

• ctx.predecessorEdge = Anderson4D.r322AnalyticPredecessorEdge ctx.state ctx.step ⋯

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

Equations

• ctx.outgoingEdge = Anderson4D.r322AnalyticOutgoingEdge ctx.step ⋯

noncomputable def Anderson4D.R322AnalyticProperStepContext.localIntegrand {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ℝ

Standard-coordinate signed integrand for this sparse proper block.

Equations

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

noncomputable def Anderson4D.R322AnalyticProperStepContext.localSpatialIntegral {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (lam ε : ℝ) (u : T4) : ℝ

The actual signed spatial integral paid by this step.

Equations

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

noncomputable def Anderson4D.R322AnalyticProperStepContext.nextState {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (lam ε : ℝ) : R322AnalyticEdgeState q hq

State after inserting the primitive difference kernel at the sparse predecessor slot.

Equations

• ctx.nextState ρ lam ε = ctx.state.updateProper ctx.pairing ⋯ ctx.suffix ctx.step ⋯ ⋯ (Anderson4D.primitiveKernelDiff ρ lam ε (Anderson4D.residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges)

theorem Anderson4D.R322AnalyticProperStepContext.localSpatialIntegral_eq_nextState_predecessor {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (lam ε : ℝ) (u : T4) (hstandard : MeasureTheory.Integrable (ctx.localIntegrand ρ ε u) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) : ctx.localSpatialIntegral ρ lam ε u = (ctx.nextState ρ lam ε).edges ctx.predecessorEdge u

One signed proper-block spatial integral is exactly the new heterogeneous predecessor edge.

theorem Anderson4D.R322AnalyticProperStepContext.eventually_localSpatialIntegral_eq_nextState_predecessor {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (lam ε : ℝ) (hstandard : ∀ᵐ (u : T4) ∂paperMeasure, MeasureTheory.Integrable (ctx.localIntegrand ρ ε u) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) : ∀ᵐ (u : T4) ∂paperMeasure, ctx.localSpatialIntegral ρ lam ε u = (ctx.nextState ρ lam ε).edges ctx.predecessorEdge u

A.e. wrapper used by the outer Fubini induction. No global ∀ u section-integrability claim is introduced.