One-step transport of a complete R-324 within-half residual integrand

This module compares the complete sparse residual integrand before and after one genuine head collapse. It starts with the geometry that identifies the new sparse successor of the absorbed predecessor edge.

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_active {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).state.active = res.state.active \ head.2

The post-head active carrier is the literal set difference by the head block.

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessorCandidates_afterHead_predecessor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeSuccessorCandidates (r324WithinHalfPredecessorSlot res.state head) = res.edgeSuccessorCandidates (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot

Seen from the old predecessor, deleting the current block leaves exactly the same candidate vertices as looking to the right of the old outgoing slot.

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessor_afterHead_predecessor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeSuccessor (r324WithinHalfPredecessorSlot res.state head) = res.edgeSuccessor (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot

The sparse successor of the absorbed predecessor is exactly the old successor beyond the outgoing head edge.

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessorCandidates_afterHead_later {ρ : 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) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeSuccessorCandidates (r324InternalVertexEdgeSlot later.1.2) = res.edgeSuccessorCandidates (r324InternalVertexEdgeSlot later.1.2)

Removing the current head does not change successor candidates of any later outgoing edge: every removed head vertex lies strictly to its left.

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessor_afterHead_later {ρ : 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) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeSuccessor (r324InternalVertexEdgeSlot later.1.2) = res.edgeSuccessor (r324InternalVertexEdgeSlot later.1.2)

Consequently every later outgoing edge has the same sparse successor before and after the head collapse.

theorem Anderson4D.R324WithinHalfResidualPrefix.tail_step_endpoints_mem_afterHead_active {ρ : 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) : later.1.1 ∈ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).state.active ∧ later.1.2 ∈ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).state.active

Every endpoint of a later suffix step already survives immediately after the current head is removed.

theorem Anderson4D.R324WithinHalfResidualPrefix.tail_step_block_subset_afterHead_active {ρ : 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) : later.2 ⊆ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).state.active

In fact the entire extraction block of every later suffix step already survives immediately after the current head.

theorem Anderson4D.R324WithinHalfResidualPrefix.later_outgoingSlot_ne_predecessor {ρ : 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) : r324InternalVertexEdgeSlot later.1.2 ≠ r324WithinHalfPredecessorSlot res.state head

A later outgoing slot is distinct from the predecessor updated by the current head.

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_edges_later_outgoing {ρ : 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) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).state.edges (r324InternalVertexEdgeSlot later.1.2) = res.state.edges (r324InternalVertexEdgeSlot later.1.2)

Absorbing the head leaves every later outgoing named edge unchanged.

theorem Anderson4D.R324WithinHalfResidualPrefix.assemble_split_afterHead_edgeSuccessor_eq {ρ : 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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (edge : Fin (m + 1)) : assemble x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeSuccessor edge) = assemble x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeSuccessor edge)

Every post-head sparse successor is read identically by the exact pre-head split tuple and by the post-head reconstruction.

theorem Anderson4D.R324WithinHalfResidualPrefix.assemble_split_later_endpoints_eq_afterHead {ρ : 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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (later : R322ExtractionStep m) (hlater : later ∈ tail) : assemble x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) (varIdx later.1.1) = assemble x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) (varIdx later.1.1) ∧ assemble x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) (varIdx later.1.2) = assemble x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) (varIdx later.1.2)

The exact split and post reconstruction agree at both endpoints of any later suffix step.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualStepDifference_later_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) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (later : R322ExtractionStep m) (hlater : later ∈ tail) : res.residualStepDifference x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) later = (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualStepDifference x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) later

A later signed residual difference is unchanged by the head collapse and reads only the post-head coordinates.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualDifferenceProduct_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) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) : res.residualDifferenceProduct x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = res.residualStepDifference x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) head * (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualDifferenceProduct x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v)

The full remaining signed-difference product splits into the literal head difference and the post-head suffix product.

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

Length form of the literal head/suffix decomposition.

theorem Anderson4D.R324WithinHalfResidualPrefix.remainingBlockIndex_cast_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : res.remainingBlockIndex ((finCongr ⋯).symm 0) = (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).blockIndex

Under the canonical finite-index cast, index zero of the old remaining list is the current head block.

theorem Anderson4D.R324WithinHalfResidualPrefix.remainingBlockIndex_cast_succ {ρ : 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 tail.length) : res.remainingBlockIndex ((finCongr ⋯).symm j.succ) = (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).remainingBlockIndex j

Positive finite indices of the old remaining list are exactly the post-head remaining block indices.

theorem Anderson4D.R324WithinHalfResidualPrefix.extractionBlockPrimitiveSum_later_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) (ε' : ℝ) (B : ExtractionBlockIndex pairing) (later : R322ExtractionStep m) (hlater : later ∈ tail) (hB : ↑B = later.2) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) : r322ExtractionBlockPrimitiveSum ρ' ε' pairing B (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = r322ExtractionBlockPrimitiveSum ρ' ε' pairing B ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v)

The complete primitive sum of any later block is independent of all head coordinates in the exact split.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualPrimitiveProduct_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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) : res.residualPrimitiveProduct ρ' ε' (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = r322ExtractionBlockPrimitiveSum ρ' ε' pairing (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).blockIndex (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) * (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualPrimitiveProduct ρ' ε' ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v)

The complete remaining primitive-coordinate product splits into the current head block and the post-head suffix product.

Ordinary sparse-chain partition

def Anderson4D.R324WithinHalfResidualPrefix.headInternalSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : Finset (Fin (m + 1))

The ordinary edge slots internal to the current head block.

Equations

• res.headInternalSlots head tail hremaining = Finset.image (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).internalSlot Finset.univ

def Anderson4D.R324WithinHalfResidualPrefix.headChainSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : Finset (Fin (m + 1))

The predecessor together with every ordinary internal head slot.

Equations

• res.headChainSlots head tail hremaining = {Anderson4D.r324WithinHalfPredecessorSlot res.state head} ∪ res.headInternalSlots head tail hremaining

theorem Anderson4D.R324WithinHalfResidualPrefix.internalSlot_injective {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : Function.Injective (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).internalSlot

Distinct standard internal indices give distinct ambient edge slots.

theorem Anderson4D.R324WithinHalfResidualPrefix.predecessorSlot_lt_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)) : r324WithinHalfPredecessorSlot res.state head < (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).internalSlot j

The predecessor lies strictly to the left of every internal head slot.

theorem Anderson4D.R324WithinHalfResidualPrefix.predecessorSlot_not_mem_headInternalSlots {ρ : 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.headInternalSlots head tail hremaining

theorem Anderson4D.R324WithinHalfResidualPrefix.prod_headInternalSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (f : Fin (m + 1) → ℝ) : ∏ edge ∈ res.headInternalSlots head tail hremaining, f edge = ∏ j : Fin (2 * residualBlockOrder head.2 - 1), f ((Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).internalSlot j)

Product reindexing from the internal-slot image back to standard primitive-chain indices.

theorem Anderson4D.R324WithinHalfResidualPrefix.prod_headChainSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (f : Fin (m + 1) → ℝ) : ∏ edge ∈ res.headChainSlots head tail hremaining, f edge = f (r324WithinHalfPredecessorSlot res.state head) * ∏ j : Fin (2 * residualBlockOrder head.2 - 1), f ((Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).internalSlot j)

The local-slot product is the predecessor factor followed by the standard internal-chain product.

theorem Anderson4D.R324WithinHalfResidualPrefix.internalSlot_not_mem_afterHead_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)) : (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).internalSlot j ∉ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).activeEdgeSlots

Every internal head slot is inactive after the head block is removed.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_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)) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualChainEdgeFactor x y v ((Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).internalSlot j) = 1

Thus every post-head ordinary internal factor is one.

theorem Anderson4D.R324WithinHalfResidualPrefix.prod_headChainSlots_before {ρ : 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) : ∏ edge ∈ res.headChainSlots head tail hremaining, res.residualChainEdgeFactor x y v edge = res.residualChainEdgeFactor x y v (r324WithinHalfPredecessorSlot res.state head) * res.headInternalChainProduct head tail hremaining x y v

The old local-slot product is exactly the incoming factor times the standard internal-chain product.

theorem Anderson4D.R324WithinHalfResidualPrefix.prod_headChainSlots_after {ρ : 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) : ∏ edge ∈ res.headChainSlots head tail hremaining, (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualChainEdgeFactor x y v edge = (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualChainEdgeFactor x y v (r324WithinHalfPredecessorSlot res.state head)

The post-head local-slot product consists only of the updated predecessor factor.

theorem Anderson4D.R324WithinHalfResidualPrefix.internalVertexEdgeSlot_mem_headInternalSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (i : Fin m) (hi : i ∈ head.2) (hne : i ≠ head.1.2) : r324InternalVertexEdgeSlot i ∈ res.headInternalSlots head tail hremaining

Every head-block vertex except the right endpoint contributes one of the standard internal ordinary slots.

theorem Anderson4D.R324WithinHalfResidualPrefix.mem_afterHead_activeEdgeSlots_of_outer {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (edge : Fin (m + 1)) (hactive : edge ∈ res.activeEdgeSlots) (hinternal : edge ∉ res.headInternalSlots head tail hremaining) (hout : edge ≠ (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot) : edge ∈ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).activeEdgeSlots

Outside the local predecessor/internal slots and the reserved head outgoing slot, every old active edge remains active after the head.

theorem Anderson4D.R324WithinHalfResidualPrefix.mem_remainingOutgoingSlots_iff_afterHead {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (edge : Fin (m + 1)) (hout : edge ≠ (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot) : edge ∈ res.remainingOutgoingSlots ↔ edge ∈ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).remainingOutgoingSlots

Away from the head outgoing slot, the reserved outgoing-slot list is identical before and after the head.

theorem Anderson4D.R324WithinHalfResidualPrefix.outer_active_edge_dichotomy {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (edge : Fin (m + 1)) (hactive : edge ∈ res.activeEdgeSlots) (hpred : edge ≠ r324WithinHalfPredecessorSlot res.state head) (hinternal : edge ∉ res.headInternalSlots head tail hremaining) (hout : edge ≠ (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot) : edge < r324WithinHalfPredecessorSlot res.state head ∨ (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot < edge

An active ordinary edge outside the local slots lies either strictly before the predecessor or strictly after the head outgoing slot.

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessor_vertex_not_mem_head_of_lt_predecessor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (edge : Fin (m + 1)) (hedge : edge < r324WithinHalfPredecessorSlot res.state head) (i : Fin m) (hsuccessor : res.edgeSuccessor edge = varIdx i) : i ∉ head.2

If an edge lies before the old predecessor, its old sparse successor cannot belong to the head block.

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessor_afterHead_outer {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (edge : Fin (m + 1)) (hactive : edge ∈ res.activeEdgeSlots) (hpred : edge ≠ r324WithinHalfPredecessorSlot res.state head) (hinternal : edge ∉ res.headInternalSlots head tail hremaining) (hout : edge ≠ (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeSuccessor edge = res.edgeSuccessor edge

Every evaluated ordinary outer edge has the same sparse successor after the head block is removed.

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_activeEdgeSlots_subset {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).activeEdgeSlots ⊆ res.activeEdgeSlots

Post-head active edge slots form a subset of the old active edge slots.

theorem Anderson4D.R324WithinHalfResidualPrefix.outgoingSlot_not_mem_afterHead_activeEdgeSlots {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot ∉ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).activeEdgeSlots

The head outgoing slot is inactive after the head block is removed.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_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) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualChainEdgeFactor x y v (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot = 1

Therefore the post-head outgoing ordinary factor is one.

theorem Anderson4D.R324WithinHalfResidualPrefix.assemble_split_activeEdge_castSucc_eq_afterHead {ρ : 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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (edge : Fin (m + 1)) (hactive : edge ∈ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).activeEdgeSlots) : assemble x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) edge.castSucc = assemble x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) edge.castSucc

Exact pre/post reconstructions agree at the left vertex of every post-head active edge.

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeDisplacement_reconstruct_split_outer {ρ : 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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (edge : Fin (m + 1)) (hactive : edge ∈ res.activeEdgeSlots) (hpred : edge ≠ r324WithinHalfPredecessorSlot res.state head) (hinternal : edge ∉ res.headInternalSlots head tail hremaining) (hout : edge ≠ (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).outgoingSlot) : res.edgeDisplacement x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) edge = (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeDisplacement x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) edge

Every ordinary outer edge reads the same spatial displacement before and after the head collapse.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainEdgeFactor_reconstruct_split_outer {ρ : 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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (edge : Fin (m + 1)) (houter : edge ∉ res.headChainSlots head tail hremaining) : res.residualChainEdgeFactor x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) edge = (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualChainEdgeFactor x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) edge

Every ordinary edge outside the local predecessor/internal slots has the same factor before and after the head collapse.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.headOuterChainProductBefore {ρ : 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) : ℝ

Ordinary outer-chain product before the head collapse.

Equations

• res.headOuterChainProductBefore head tail hremaining x y v = ∏ edge ∈ Finset.univ \ res.headChainSlots head tail hremaining, res.residualChainEdgeFactor x y v edge

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.headOuterChainProductAfter {ρ : 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) : ℝ

Ordinary outer-chain product after the head collapse.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.headOuterChainProductBefore_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) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) : res.headOuterChainProductBefore head tail hremaining x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = res.headOuterChainProductAfter head tail hremaining x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v)

The ordinary outer-chain product is independent of the head coordinates and unchanged by the collapse.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainProduct_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) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) : res.residualChainProduct x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = res.residualChainEdgeFactor x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) (r324WithinHalfPredecessorSlot res.state head) * res.headInternalChainProduct head tail hremaining x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) * res.headOuterChainProductAfter head tail hremaining x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v)

Exact ordinary-chain factorization before the head collapse.

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_residualChainProduct {ρ : 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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualChainProduct x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) = (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualChainEdgeFactor x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) (r324WithinHalfPredecessorSlot res.state head) * res.headOuterChainProductAfter head tail hremaining x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v)

Exact ordinary-chain factorization after the head collapse.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.headOuterFactor {ρ : 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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) → ℝ

All factors independent of the current head coordinates, expressed in the actual post-head residual state.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.residualIntegrand_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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) : res.residualIntegrand ρ✝ ε✝ x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) = res.headLocalFactor head tail hremaining ρ✝ ε✝ x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) * res.headOuterFactor head tail hremaining ρ✝ ε✝ x y v

The complete pre-head residual integrand is exactly the genuine local head factor times a post-coordinate outer factor.

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_residualIntegrand {ρ : 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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualIntegrand ρ✝ ε✝ x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) = (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualChainEdgeFactor x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) (r324WithinHalfPredecessorSlot res.state head) * res.headOuterFactor head tail hremaining ρ✝ ε✝ x y v

The complete post-head residual integrand is the updated predecessor factor times the same outer factor.

theorem Anderson4D.R324WithinHalfResidualPrefix.predecessorSlot_mem_afterHead_activeEdgeSlots {ρ : 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 ∈ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).activeEdgeSlots

The old predecessor slot survives as an ordinary active edge after the head block is removed.

theorem Anderson4D.R324WithinHalfResidualPrefix.predecessorSlot_not_mem_afterHead_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 ∉ (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).remainingOutgoingSlots

No later reserved outgoing edge is the old predecessor slot.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_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) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualChainEdgeFactor x y v (r324WithinHalfPredecessorSlot res.state head) = (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).state.edges (r324WithinHalfPredecessorSlot res.state head) ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeDisplacement x y v (r324WithinHalfPredecessorSlot res.state head))

Consequently the post-head sparse predecessor factor is the updated named edge, without an indicator or reserved-slot branch.

theorem Anderson4D.R324WithinHalfResidualPrefix.headOuterBase_eq_afterHead_reconstruct {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (i : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate) : res.headOuterBase head tail hremaining v ↑i = (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v ↑i

A post-surviving internal coordinate has the same value in the zero-filled pre-head base and in the actual post-head reconstruction.

theorem Anderson4D.R324WithinHalfResidualPrefix.assemble_afterHead_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) (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) : assemble x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) (r324WithinHalfPredecessorSlot res.state head).castSucc = res.headPredecessorPoint head tail hremaining x y v

The post-head predecessor point is the named outer predecessor point used by the translated local collapse.

theorem Anderson4D.R324WithinHalfResidualPrefix.assemble_headOuterBase_edgeSuccessor_eq_afterHead {ρ : 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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (edge : Fin (m + 1)) : assemble x y (res.headOuterBase head tail hremaining v) ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeSuccessor edge) = assemble x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeSuccessor edge)

Every post-head sparse successor is read identically from the pre-head outer base and from the post-head reconstruction.

theorem Anderson4D.R324WithinHalfResidualPrefix.assemble_afterHead_edgeSuccessor_predecessor_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) (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) : assemble x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeSuccessor (r324WithinHalfPredecessorSlot res.state head)) = res.headSuccessorPoint head tail hremaining x y v

The post-head sparse successor point of the absorbed predecessor is the outer successor point used by the local collapse.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_edgeDisplacement_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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).edgeDisplacement x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) (r324WithinHalfPredecessorSlot res.state head) = res.headPredecessorPoint head tail hremaining x y v - res.headSuccessorPoint head tail hremaining x y v

The post-head displacement of the absorbed predecessor is exactly the relative point at which the local collapse returns its updated edge.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_residualChainEdgeFactor_predecessor_reconstruct {ρ : 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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualChainEdgeFactor x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) (r324WithinHalfPredecessorSlot res.state head) = (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).state.edges (r324WithinHalfPredecessorSlot res.state head) (res.headPredecessorPoint head tail hremaining x y v - res.headSuccessorPoint head tail hremaining x y v)

The actual post-head predecessor factor is exactly the updated edge at the translated local-collapse point.

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_head_rawLocal_sub_const_mul_complex {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (u a : T4) (outer : ℂ) : (∫ (actual : Fin (2 * residualBlockOrder head.2) → T4), ↑((Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).rawLocalIntegrand ρ ε u fun (i : Fin (2 * residualBlockOrder (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).step.2)) => actual i - a) * outer ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure) = ∫ (t : Fin (2 * residualBlockOrder head.2) → T4), ↑((Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).rawLocalIntegrand ρ ε u t) * outer ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure

Head-typed wrapper around product-Haar translation invariance. Keeping the literal head.2 carrier in this interface avoids leaking the reducible headContext.step field into the physical residual statement.

theorem Anderson4D.R324WithinHalfResidualPrefix.lamEps_pow_integral_headLocalFactor_eq_afterHead_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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (outer : ℂ) (hstandard : MeasureTheory.Integrable ((Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).localIntegrand ρ ε (res.headPredecessorPoint head tail hremaining x y v - res.headSuccessorPoint head tail hremaining x y v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 w)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * residualBlockOrder head.2) * ∫ (t : Fin (2 * residualBlockOrder head.2) → T4), ↑(res.headLocalFactor head tail hremaining ρ ε x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)))) * outer ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure) = ↑((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualChainEdgeFactor x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v) (r324WithinHalfPredecessorSlot res.state head)) * outer

One physical head section.

After the exact coordinate split, integrating the genuine four-factor head section replaces it by the predecessor factor of the absorbed residual state. The arbitrary complex outer factor is fixed throughout the local integral.

theorem Anderson4D.R324WithinHalfResidualPrefix.lamEps_pow_integral_residualIntegrand_section_eq_afterHead {ρ : 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 : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4) (hstandard : MeasureTheory.Integrable ((Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).localIntegrand ρ ε (res.headPredecessorPoint head tail hremaining x y v - res.headSuccessorPoint head tail hremaining x y v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 w)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * residualBlockOrder head.2) * ∫ (t : Fin (2 * residualBlockOrder head.2) → T4), ↑(res.residualIntegrand ρ ε x y (res.reconstruct ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)))) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure) = ↑((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualIntegrand ρ ε x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v))

Complete one-head residual section transition.

At fixed post-head coordinates, the exact perturbative power times the complete pre-head residual section integral is the complete post-head residual integrand.

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_splitSurviving_post_first {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (res.SurvivingCoordinate → T4) → E) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) : (∫ (w : res.SurvivingCoordinate → T4), f w ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ∫ (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4), ∫ (t : Fin (2 * residualBlockOrder head.2) → T4), f ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate) => paperMeasure

Fubini for the exact head/post split, with the post coordinates on the outside. This is the order consumed by the one-section transition above.

theorem Anderson4D.R324WithinHalfResidualPrefix.lamEps_pow_integral_residual_eq_afterHead {ρ : 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) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => ↑(res.residualIntegrand ρ ε x y (res.reconstruct w))) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) (hstandard : ∀ (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4), MeasureTheory.Integrable ((Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).localIntegrand ρ ε (res.headPredecessorPoint head tail hremaining x y v - res.headSuccessorPoint head tail hremaining x y v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).step.2)) => paperMeasure)) (hinternal : ∀ (_v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4), ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 w)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (w : res.SurvivingCoordinate → T4), ↑(res.residualIntegrand ρ ε x y (res.reconstruct w)) ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).remainingOrder) * ∫ (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4), ↑((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualIntegrand ρ ε x y ((Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).reconstruct v)) ∂MeasureTheory.Measure.pi fun (x : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate) => paperMeasure

Complete one-head residual-value transition, complex form.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualValue_eq_afterHead {ρ : 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) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => ↑(res.residualIntegrand ρ ε x y (res.reconstruct w))) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) (hstandard : ∀ (v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4), MeasureTheory.Integrable ((Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).localIntegrand ρ ε (res.headPredecessorPoint head tail hremaining x y v - res.headSuccessorPoint head tail hremaining x y v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).step.2)) => paperMeasure)) (hinternal : ∀ (_v : (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).SurvivingCoordinate → T4), ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (Anderson4D.R324WithinHalfResidualPrefix.ctx✝ res head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 w)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : res.residualValue ρ lam ε x y = (Anderson4D.R324WithinHalfResidualPrefix.post✝ res head tail hremaining).residualValue ρ lam ε x y

Real scalar form of the complete one-head residual-value transition.

Exact iteration through the complete remaining suffix

structure Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfResidualStepReady {ρ : 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) : Prop

The precise Fubini and local-collapse evidence needed for one literal head of a reachable within-half residual prefix. Packaging these three facts keeps the list iteration below independent of how integrability is established (globally from the original moment integrand, or locally from a tree majorant).

• full : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => ↑(res.residualIntegrand ρ ε x y (res.reconstruct w))) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)
• standard (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : MeasureTheory.Integrable ((res.headContext head tail hremaining).localIntegrand ρ ε (res.headPredecessorPoint head tail hremaining x y v - res.headSuccessorPoint head tail hremaining x y v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2)) => paperMeasure)
• internal (_v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 w)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfResidualStepReady.value_eq_afterHead {ρ : 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} (ready : res.R324WithinHalfResidualStepReady head tail hremaining x y) : res.residualValue ρ lam ε x y = (res.afterHead head tail hremaining).residualValue ρ lam ε x y

One packaged ready step preserves the complete residual value.

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfResidualStepProvider {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (x y : T4) : Prop

Integrability provider for every genuine nonempty suffix. This is the single analytic datum consumed by the structural list iteration.

Equations

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

inductive Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfResidualIterationReady {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (x y : T4) : R324WithinHalfResidualPrefix ρ lam ε pairing → Prop

A proof-relevant exact trace through every remaining schedule block.

• terminal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {x y : T4} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) : R324WithinHalfResidualIterationReady x y res
• step {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {x y : T4} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (ready : res.R324WithinHalfResidualStepReady head tail hremaining x y) (next : R324WithinHalfResidualIterationReady x y (res.afterHead head tail hremaining)) : R324WithinHalfResidualIterationReady x y res

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfResidualIterationReady.of_provider {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (x y : T4) (provider : R324WithinHalfResidualStepProvider x y) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : R324WithinHalfResidualIterationReady x y res

A uniform step provider constructs the complete proof-relevant trace. The recursion is on the literal remaining suffix, whose tail is definitionally the suffix of afterHead.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfResidualIterationReady.exists_terminal_value_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {x y : T4} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} (ready : R324WithinHalfResidualIterationReady x y res) : ∃ (terminal : R324WithinHalfResidualPrefix ρ lam ε pairing), terminal.remaining = [] ∧ terminal.state.processed = r322AnalyticSchedule pairing ∧ res.residualValue ρ lam ε x y = terminal.residualValue ρ lam ε x y

Iterating a ready trace reaches a genuine empty suffix and preserves the complete residual value exactly.

theorem Anderson4D.R324WithinHalfResidualPrefix.exists_terminal_residualValue_eq_of_provider {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (x y : T4) (provider : R324WithinHalfResidualStepProvider x y) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : ∃ (terminal : R324WithinHalfResidualPrefix ρ lam ε pairing), terminal.remaining = [] ∧ terminal.state.processed = r322AnalyticSchedule pairing ∧ res.residualValue ρ lam ε x y = terminal.residualValue ρ lam ε x y

Consumer-facing list iteration from one uniform step provider.