Heterogeneous edge states for an R-324 within-half prefix

def Anderson4D.r324InternalVertexEdgeSlot {m : ℕ} (i : Fin m) : Fin (m + 1)

Edge slot immediately to the left of an internal pairing vertex.

Equations

• Anderson4D.r324InternalVertexEdgeSlot i = ⟨↑i + 1, ⋯⟩

structure Anderson4D.R324WithinHalfEdgeState (m : ℕ) : Type

A processed analytic prefix together with its current named kernels.

• processed : List (R322ExtractionStep m)
• edges : Fin (m + 1) → T4 → ℝ

noncomputable def Anderson4D.r324InitialWithinHalfEdgeState (m : ℕ) : R324WithinHalfEdgeState m

Equations

• Anderson4D.r324InitialWithinHalfEdgeState m = { processed := [], edges := fun (x : Fin (m + 1)) => Anderson4D.greenFn }

def Anderson4D.R324WithinHalfEdgeState.active {m : ℕ} (state : R324WithinHalfEdgeState m) : Finset (Fin m)

Equations

• state.active = Anderson4D.r322AnalyticActiveCarrier state.processed

def Anderson4D.r324WithinHalfPredecessorCandidates {m : ℕ} (state : R324WithinHalfEdgeState m) (step : R322ExtractionStep m) : Finset (Fin (m + 1))

Candidate chain slots before a current block. Slot zero is the incoming external edge, so this set is always nonempty.

Equations

• Anderson4D.r324WithinHalfPredecessorCandidates state step = {0} ∪ Finset.image Anderson4D.r324InternalVertexEdgeSlot ({i ∈ state.active | i < step.1.1})

theorem Anderson4D.r324WithinHalfPredecessorCandidates_nonempty {m : ℕ} (state : R324WithinHalfEdgeState m) (step : R322ExtractionStep m) : (r324WithinHalfPredecessorCandidates state step).Nonempty

def Anderson4D.r324WithinHalfPredecessorSlot {m : ℕ} (state : R324WithinHalfEdgeState m) (step : R322ExtractionStep m) : Fin (m + 1)

Greatest surviving edge slot before the current block.

Equations

• Anderson4D.r324WithinHalfPredecessorSlot state step = (Anderson4D.r324WithinHalfPredecessorCandidates state step).max' ⋯

structure Anderson4D.R324WithinHalfStepContext {m : ℕ} (pairing : PartialPairing (Fin m)) : Type

Certified next step of the actual analytic schedule.

• state : R324WithinHalfEdgeState m
• step : R322ExtractionStep m
• suffix : List (R322ExtractionStep m)
• schedule_eq : r322AnalyticSchedule pairing = self.state.processed ++ self.step :: self.suffix

theorem Anderson4D.R324WithinHalfStepContext.step_mem_schedule {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) : ctx.step ∈ r322AnalyticSchedule pairing

theorem Anderson4D.R324WithinHalfStepContext.block_mem_extractionBlocks {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) : ctx.step.2 ∈ extractionBlocks pairing

theorem Anderson4D.R324WithinHalfStepContext.blockFullyPaired {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) : IsFullyPairedOn pairing ctx.step.2

theorem Anderson4D.R324WithinHalfStepContext.blockNonempty {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) : ctx.step.2.Nonempty

theorem Anderson4D.R324WithinHalfStepContext.one_le_blockOrder {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) : 1 ≤ residualBlockOrder ctx.step.2

def Anderson4D.R324WithinHalfStepContext.blockOrderIso {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) : Fin (2 * residualBlockOrder ctx.step.2) ≃o ↥ctx.step.2

Equations

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

def Anderson4D.R324WithinHalfStepContext.internalSlot {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (j : Fin (2 * residualBlockOrder ctx.step.2 - 1)) : Fin (m + 1)

State slot carrying the jth internal edge of the current sparse block.

Equations

• ctx.internalSlot j = Anderson4D.r324InternalVertexEdgeSlot ↑(ctx.blockOrderIso ⟨↑j, ⋯⟩)

def Anderson4D.R324WithinHalfStepContext.internalEdges {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) : Fin (2 * residualBlockOrder ctx.step.2 - 1) → T4 → ℝ

Equations

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

noncomputable def Anderson4D.R324WithinHalfStepContext.primitiveKernel {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (lam ε : ℝ) : T4 → ℝ

Deterministic primitive kernel generated by the current block.

Equations

• ctx.primitiveKernel ρ lam ε = Anderson4D.primitiveKernelDiff ρ lam ε (Anderson4D.residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges

def Anderson4D.R324WithinHalfStepContext.outgoingSlot {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) : Fin (m + 1)

Current edge immediately leaving the block.

Equations

• ctx.outgoingSlot = Anderson4D.r324InternalVertexEdgeSlot ctx.step.1.2

noncomputable def Anderson4D.R324WithinHalfStepContext.collapsedKernel {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (lam ε : ℝ) : T4 → ℝ

The genuine block collapse: predecessor, primitive kernel, and the difference across the current outgoing kernel are integrated as in (4.8).

Equations

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

noncomputable def Anderson4D.R324WithinHalfStepContext.absorb {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (lam ε : ℝ) : R324WithinHalfEdgeState m

Absorb one actual schedule step at its surviving predecessor slot, leaving every other named edge unchanged.

Equations

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

@[simp]

theorem Anderson4D.R324WithinHalfStepContext.absorb_edges_predecessor {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (lam ε : ℝ) : (ctx.absorb ρ lam ε).edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) = ctx.collapsedKernel ρ lam ε

theorem Anderson4D.R324WithinHalfStepContext.absorb_edges_of_ne {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (lam ε : ℝ) (edge : Fin (m + 1)) (hne : edge ≠ r324WithinHalfPredecessorSlot ctx.state ctx.step) : (ctx.absorb ρ lam ε).edges edge = ctx.state.edges edge

@[simp]

theorem Anderson4D.R324WithinHalfStepContext.absorb_active {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (lam ε : ℝ) : (ctx.absorb ρ lam ε).active = ctx.state.active \ ctx.step.2

inductive Anderson4D.R324WithinHalfStateReachable {m : ℕ} (pairing : PartialPairing (Fin m)) (ρ : SmoothCutoff) (lam ε : ℝ) : R324WithinHalfEdgeState m → Prop

Algebraically reachable states are generated only by actual successive steps of the fixed analytic schedule and the genuine three-kernel collapse above. No desired pointwise factorization is stored in this predicate.

• initial {m : ℕ} {pairing : PartialPairing (Fin m)} {ρ : SmoothCutoff} {lam ε : ℝ} : R324WithinHalfStateReachable pairing ρ lam ε (r324InitialWithinHalfEdgeState m)
• absorb {m : ℕ} {pairing : PartialPairing (Fin m)} {ρ : SmoothCutoff} {lam ε : ℝ} (ctx : R324WithinHalfStepContext pairing) (hctx : R324WithinHalfStateReachable pairing ρ lam ε ctx.state) : R324WithinHalfStateReachable pairing ρ lam ε (ctx.absorb ρ lam ε)

The empty-prefix predecessor is genuinely free Green

theorem Anderson4D.firstLeft_predecessor_not_extracted_of_analyticHead {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule e₀.fst = r324FirstLeftSelectedStep e₀ hleft :: tail) : r324FirstLeftPredecessorEdge e₀ hleft ∉ extractedRightEdges e₀.fst

theorem Anderson4D.productionPredecessor_eq_initialStateEdge {m : ℕ} (κ : PartialPairing (Fin m)) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (hsig : reductionEndpointSignature κ = reductionEndpointSignature e₀.fst) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule e₀.fst = r324FirstLeftSelectedStep e₀ hleft :: tail) (xt : Fin (m + 2) → T4) : r324ProductionGreenEdgeFactor κ xt (r324FirstLeftPredecessorEdge e₀ hleft) = ↑((r324InitialWithinHalfEdgeState m).edges (r324FirstLeftPredecessorEdge e₀ hleft) (xt (r324FirstLeftPredecessorEdge e₀ hleft).castSucc - xt (r324FirstLeftPredecessorEdge e₀ hleft).succ))

theorem Anderson4D.r324FirstLeftReconstruct_touchingGreenProduct_eq_initialStateLocal {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule e₀.fst = r324FirstLeftSelectedStep e₀ hleft :: tail) (xt : Fin (m + 2) → T4) : have κ := (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst; r324FirstLeftTouchingGreenProduct κ e₀ hleft xt = ↑((r324InitialWithinHalfEdgeState m).edges (r324FirstLeftPredecessorEdge e₀ hleft) (xt (r324FirstLeftPredecessorEdge e₀ hleft).castSucc - xt (r324FirstLeftPredecessorEdge e₀ hleft).succ)) * ↑(primitiveChainProduct (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ⋯ (fun (x : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft) - 1)) => greenFn) (r324FirstLeftCarrierTuple e₀ hleft xt)) * r324ProductionGreenEdgeFactor κ xt (r324FirstLeftOutgoingEdge e₀ hleft)