Complete surviving integrand of one R-324 within-half prefix

This module names the full sparse-chain integrand which survives a genuine processed prefix. Its coordinate carrier is the one proved measure-preserving in R324WithinHalfResidualCoordinates.

The three factors are kept separate:

• ordinary heterogeneous edges on the sparse active chain;
• the signed outgoing-edge differences of every remaining schedule step;
• one complete primitive-pairing sum for every remaining block.

This is pre-collapse data. No original unintegrated integrand is equated with a post-collapse edge state.

theorem Anderson4D.R324WithinHalfStepContext.blockOrderIso_zero {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) : ↑(ctx.blockOrderIso ⟨0, ⋯⟩) = ctx.step.1.1

The first standard coordinate of a current within-half block is its certified left endpoint.

theorem Anderson4D.R324WithinHalfStepContext.blockOrderIso_last {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) : ↑(ctx.blockOrderIso (primitiveLast (residualBlockOrder ctx.step.2) ⋯)) = ctx.step.1.2

The last standard coordinate of a current within-half block is its certified right endpoint.

theorem Anderson4D.R324WithinHalfStepContext.internalSlot_lt_outgoingSlot {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (j : Fin (2 * residualBlockOrder ctx.step.2 - 1)) : ctx.internalSlot j < ctx.outgoingSlot

Every genuine internal standard edge precedes the outgoing slot of its block.

theorem Anderson4D.R324WithinHalfStepContext.rawLocalIntegrand_translated {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (ε : ℝ) (u a : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : (ctx.rawLocalIntegrand ρ ε (u - a) fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => t j - a) = ctx.state.edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) (u - t ⟨0, ⋯⟩) * primitiveChainProduct (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges t * (ctx.state.edges ctx.outgoingSlot (t (primitiveLast (residualBlockOrder ctx.step.2) ⋯) - a) - ctx.state.edges ctx.outgoingSlot (t ⟨0, ⋯⟩ - a)) * ∑ κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2)), primitiveCovarianceProduct ρ ε (residualBlockOrder ctx.step.2) (↑κB) t

Translating all local coordinates and the predecessor point by one common torus point gives an explicit absolute-coordinate form of the raw local integrand.

Sparse production-chain geometry

def Anderson4D.R324WithinHalfResidualPrefix.activeEdgeSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : Finset (Fin (m + 1))

Edge slots whose left endpoint survives in the current production chain. Slot zero is the incoming external edge.

Equations

• res.activeEdgeSlots = {0} ∪ Finset.image Anderson4D.r324InternalVertexEdgeSlot res.state.active

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.zero_mem_activeEdgeSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : 0 ∈ res.activeEdgeSlots

theorem Anderson4D.R324WithinHalfResidualPrefix.internalVertexEdgeSlot_mem_activeEdgeSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (i : Fin m) (hi : i ∈ res.state.active) : r324InternalVertexEdgeSlot i ∈ res.activeEdgeSlots

def Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessorCandidates {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (edge : Fin (m + 1)) : Finset (Fin (m + 2))

Active internal vertices strictly to the right of one production edge slot, shifted into the (m+2) chain carrier. The terminal external vertex is always adjoined as a candidate.

Equations

• res.edgeSuccessorCandidates edge = {Fin.last (m + 1)} ∪ Finset.image Anderson4D.varIdx ({i ∈ res.state.active | ↑edge < ↑(Anderson4D.varIdx i)})

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessorCandidates_nonempty {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (edge : Fin (m + 1)) : (res.edgeSuccessorCandidates edge).Nonempty

def Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (edge : Fin (m + 1)) : Fin (m + 2)

Least surviving production-chain vertex strictly after an edge slot.

Equations

• res.edgeSuccessor edge = (res.edgeSuccessorCandidates edge).min' ⋯

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessor_mem_candidates {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (edge : Fin (m + 1)) : res.edgeSuccessor edge ∈ res.edgeSuccessorCandidates edge

theorem Anderson4D.R324WithinHalfResidualPrefix.edge_lt_edgeSuccessor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (edge : Fin (m + 1)) : edge.castSucc < res.edgeSuccessor edge

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.edgeDisplacement {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : Fin m → T4) (edge : Fin (m + 1)) : T4

The spatial difference read by one current heterogeneous edge.

Equations

• res.edgeDisplacement x y v edge = Anderson4D.assemble x y v edge.castSucc - Anderson4D.assemble x y v (res.edgeSuccessor edge)

def Anderson4D.R324WithinHalfResidualPrefix.remainingOutgoingSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : List (Fin (m + 1))

Outgoing production slots reserved for the signed differences of the analytic suffix.

Equations

• res.remainingOutgoingSlots = List.map (fun (step : Anderson4D.R322ExtractionStep m) => Anderson4D.r324InternalVertexEdgeSlot step.1.2) res.remaining

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.residualChainEdgeFactor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : Fin m → T4) (edge : Fin (m + 1)) : ℝ

One ordinary sparse-chain factor. Deleted left vertices and outgoing slots reserved for remaining signed differences contribute one.

Equations

• res.residualChainEdgeFactor x y v edge = if edge ∈ res.activeEdgeSlots then if edge ∈ res.remainingOutgoingSlots then 1 else res.state.edges edge (res.edgeDisplacement x y v edge) else 1

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.residualChainProduct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : Fin m → T4) : ℝ

Product of all ordinary sparse-chain factors.

Equations

• res.residualChainProduct x y v = ∏ edge : Fin (m + 1), res.residualChainEdgeFactor x y v edge

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.residualStepDifference {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : Fin m → T4) (step : R322ExtractionStep m) : ℝ

Signed outgoing-edge difference belonging to one remaining schedule step, read against its actual sparse successor.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.residualDifferenceProduct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : Fin m → T4) : ℝ

Product of all signed differences in the literal remaining schedule.

Equations

• res.residualDifferenceProduct x y v = (List.map (res.residualStepDifference x y v) res.remaining).prod

Remaining primitive coordinates

def Anderson4D.R324WithinHalfResidualPrefix.remainingBlockIndex {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (j : Fin res.remaining.length) : ExtractionBlockIndex pairing

A remaining schedule block is a genuine extraction block of the frozen within-half pairing.

Equations

• res.remainingBlockIndex j = ⟨(res.remaining.get j).2, ⋯⟩

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.residualPrimitiveProduct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : SmoothCutoff → ℝ → (v : Fin m → T4) → ℝ

Complete primitive covariance sum on every remaining block.

Equations

• res.residualPrimitiveProduct ρ ε v = ∏ j : Fin res.remaining.length, Anderson4D.r322ExtractionBlockPrimitiveSum ρ ε pairing (res.remainingBlockIndex j) v

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.residualIntegrand {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : SmoothCutoff → ℝ → (x y : T4) → (v : Fin m → T4) → ℝ

The complete pre-collapse residual integrand on the sparse within-half carrier.

Equations

• res.residualIntegrand ρ ε x y v = res.residualChainProduct x y v * res.residualDifferenceProduct x y v * res.residualPrimitiveProduct ρ ε v

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.residualValue {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : SmoothCutoff → ℝ → ℝ → (x y : T4) → ℝ

Complete scalar residual value, with only genuinely surviving internal coordinates integrated.

Equations

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

Literal head bookkeeping

theorem Anderson4D.R324WithinHalfResidualPrefix.head_one_le_blockOrder {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : 1 ≤ residualBlockOrder head.2

The literal head has positive primitive order, stated without exposing the reducible headContext.step field.

theorem Anderson4D.R324WithinHalfResidualPrefix.head_right_lt_tail_right {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (later : R322ExtractionStep m) (hlater : later ∈ tail) : head.1.2 < later.1.2

theorem Anderson4D.R324WithinHalfResidualPrefix.predecessorSlot_val_le_left {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) : ↑(r324WithinHalfPredecessorSlot res.state head) ≤ ↑head.1.1

theorem Anderson4D.R324WithinHalfResidualPrefix.predecessorSlot_lt_outgoingSlot {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : r324WithinHalfPredecessorSlot res.state head < r324InternalVertexEdgeSlot head.1.2

theorem Anderson4D.R324WithinHalfResidualPrefix.predecessorSlot_mem_activeEdgeSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) : r324WithinHalfPredecessorSlot res.state head ∈ res.activeEdgeSlots

theorem Anderson4D.R324WithinHalfResidualPrefix.predecessorSlot_not_mem_remainingOutgoingSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : r324WithinHalfPredecessorSlot res.state head ∉ res.remainingOutgoingSlots

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessor_predecessorSlot {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : res.edgeSuccessor (r324WithinHalfPredecessorSlot res.state head) = varIdx head.1.1

The sparse successor of the current predecessor slot is the first standard vertex of the current block.

theorem Anderson4D.R324WithinHalfResidualPrefix.internalSlot_mem_activeEdgeSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (j : Fin (2 * residualBlockOrder head.2 - 1)) : (res.headContext head tail hremaining).internalSlot j ∈ res.activeEdgeSlots

theorem Anderson4D.R324WithinHalfResidualPrefix.internalSlot_not_mem_remainingOutgoingSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (j : Fin (2 * residualBlockOrder head.2 - 1)) : (res.headContext head tail hremaining).internalSlot j ∉ res.remainingOutgoingSlots

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessor_internalSlot {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (j : Fin (2 * residualBlockOrder head.2 - 1)) : have jnext := ⟨↑j + 1, ⋯⟩; res.edgeSuccessor ((res.headContext head tail hremaining).internalSlot j) = varIdx ↑((res.headContext head tail hremaining).blockOrderIso jnext)

On an internal standard edge of the current block, the sparse production successor is the next standard block coordinate.

theorem Anderson4D.R324WithinHalfResidualPrefix.outgoingSlot_mem_activeEdgeSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : (res.headContext head tail hremaining).outgoingSlot ∈ res.activeEdgeSlots

theorem Anderson4D.R324WithinHalfResidualPrefix.outgoingSlot_mem_remainingOutgoingSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : (res.headContext head tail hremaining).outgoingSlot ∈ res.remainingOutgoingSlots

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainEdgeFactor_predecessor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (v : Fin m → T4) : res.residualChainEdgeFactor x y v (r324WithinHalfPredecessorSlot res.state head) = res.state.edges (r324WithinHalfPredecessorSlot res.state head) (res.edgeDisplacement x y v (r324WithinHalfPredecessorSlot res.state head))

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainEdgeFactor_internal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (v : Fin m → T4) (j : Fin (2 * residualBlockOrder head.2 - 1)) : res.residualChainEdgeFactor x y v ((res.headContext head tail hremaining).internalSlot j) = res.state.edges ((res.headContext head tail hremaining).internalSlot j) (res.edgeDisplacement x y v ((res.headContext head tail hremaining).internalSlot j))

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainEdgeFactor_outgoing {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (v : Fin m → T4) : res.residualChainEdgeFactor x y v (res.headContext head tail hremaining).outgoingSlot = 1

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.headInternalChainProduct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (v : Fin m → T4) : ℝ

Product of the ordinary sparse edges internal to the current block.

Equations

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

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainEdgeFactor_internal_split {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) (j : Fin (2 * residualBlockOrder head.2 - 1)) : res.residualChainEdgeFactor x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) ((res.headContext head tail hremaining).internalSlot j) = (res.headContext head tail hremaining).internalEdges j (t ⟨↑j, ⋯⟩ - t ⟨↑j + 1, ⋯⟩)

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.headInternalChainProduct_split {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.headInternalChainProduct head tail hremaining x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = primitiveChainProduct (residualBlockOrder head.2) ⋯ (res.headContext head tail hremaining).internalEdges t

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.headOuterBase {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : Fin m → T4

A base ambient internal tuple in which the current head coordinates are zero and the post-prefix coordinates retain their actual values.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.headSuccessorPoint {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : T4

The active successor anchoring the current outgoing difference, evaluated only from post-prefix coordinates.

Equations

• res.headSuccessorPoint head tail hremaining x y v = Anderson4D.assemble x y (res.headOuterBase head tail hremaining v) (res.edgeSuccessor (res.headContext head tail hremaining).outgoingSlot)

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.headPredecessorPoint {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : T4

The actual predecessor point of the current head, evaluated only from post-prefix coordinates.

Equations

• res.headPredecessorPoint head tail hremaining x y v = Anderson4D.assemble x y (res.headOuterBase head tail hremaining v) (Anderson4D.r324WithinHalfPredecessorSlot res.state head).castSucc

theorem Anderson4D.R324WithinHalfResidualPrefix.assemble_split_predecessor_eq_headPredecessorPoint {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : assemble x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) (r324WithinHalfPredecessorSlot res.state head).castSucc = res.headPredecessorPoint head tail hremaining x y v

The current predecessor point is independent of every head coordinate.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainEdgeFactor_predecessor_split {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.residualChainEdgeFactor x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) (r324WithinHalfPredecessorSlot res.state head) = res.state.edges (r324WithinHalfPredecessorSlot res.state head) (res.headPredecessorPoint head tail hremaining x y v - t ⟨0, ⋯⟩)

Under the exact head/post split, the incoming sparse factor is read from the post-coordinate predecessor point to the first head coordinate.

theorem Anderson4D.R324WithinHalfResidualPrefix.assemble_split_edgeSuccessor_outgoing_eq_headSuccessorPoint {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : assemble x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) (res.edgeSuccessor (res.headContext head tail hremaining).outgoingSlot) = res.headSuccessorPoint head tail hremaining x y v

The actual sparse successor of the outgoing head edge is independent of all current-head coordinates.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.standardBlockTuple_reconstruct_split {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : (res.headContext head tail hremaining).standardBlockTuple (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = t

theorem Anderson4D.R324WithinHalfResidualPrefix.extractionBlockPrimitiveSum_reconstruct_split {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (ρ✝ : SmoothCutoff) (ε✝ : ℝ) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : r322ExtractionBlockPrimitiveSum ρ✝ ε✝ pairing (res.headContext head tail hremaining).blockIndex (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = ∑ κB : ↥(primitiveFullPairings (residualBlockOrder head.2)), primitiveCovarianceProduct ρ✝ ε✝ (residualBlockOrder head.2) (↑κB) t

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.residualStepDifference_head_split {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.residualStepDifference x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) head = res.state.edges (res.headContext head tail hremaining).outgoingSlot (t (primitiveLast (residualBlockOrder head.2) ⋯) - res.headSuccessorPoint head tail hremaining x y v) - res.state.edges (res.headContext head tail hremaining).outgoingSlot (t ⟨0, ⋯⟩ - res.headSuccessorPoint head tail hremaining x y v)

The signed outgoing factor of the head reads the first and last standard head coordinates against its post-coordinate sparse successor.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.headLocalFactor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : SmoothCutoff → ℝ → (x y : T4) → (v : Fin m → T4) → ℝ

The four factors belonging to the literal head before its spatial collapse.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.primitiveChainProduct_sub_const {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (t : Fin (2 * residualBlockOrder head.2) → T4) (a : T4) : (primitiveChainProduct (residualBlockOrder head.2) ⋯ (res.headContext head tail hremaining).internalEdges fun (j : Fin (2 * residualBlockOrder head.2)) => t j - a) = primitiveChainProduct (residualBlockOrder head.2) ⋯ (res.headContext head tail hremaining).internalEdges t

Primitive chains are unchanged by translating every standard coordinate by the same torus point.

theorem Anderson4D.R324WithinHalfResidualPrefix.primitiveCovarianceProduct_sub_const {m : ℕ} (head : R322ExtractionStep m) (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin (2 * residualBlockOrder head.2))) (t : Fin (2 * residualBlockOrder head.2) → T4) (a : T4) : (primitiveCovarianceProduct ρ ε (residualBlockOrder head.2) κ fun (j : Fin (2 * residualBlockOrder head.2)) => t j - a) = primitiveCovarianceProduct ρ ε (residualBlockOrder head.2) κ t

Primitive covariance products are unchanged by translating every standard coordinate by the same torus point.

theorem Anderson4D.R324WithinHalfResidualPrefix.headLocalFactor_reconstruct_split {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (ρ✝ : SmoothCutoff) (ε✝ : ℝ) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.headLocalFactor head tail hremaining ρ✝ ε✝ x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = (res.headContext head tail hremaining).rawLocalIntegrand ρ✝ ε✝ (res.headPredecessorPoint head tail hremaining x y v - res.headSuccessorPoint head tail hremaining x y v) fun (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2)) => t j - res.headSuccessorPoint head tail hremaining x y v

Under the exact coordinate split, the literal head factors are precisely the translated raw local integrand consumed by the collapse theorem.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.remainingOutgoingSlots_head {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : res.remainingOutgoingSlots = r324InternalVertexEdgeSlot head.1.2 :: (res.afterHead head tail hremaining).remainingOutgoingSlots