Gluing the terminal half chains to a nested cross step #
This module transports the literal inside-to-outside order of the doubled residual schedule to the two terminal half chains. On the left the later carrier precedes the current head; on the right the current head precedes the later carrier. These are exactly the two orientations of the three-way half-chain partition.
Pull a doubled carrier back to the left terminal half.
Equations
- Anderson4D.r324LeftHalfPullback B = {i : Fin m | Anderson4D.leftMomentIndex i ∈ B}
Instances For
Pull a doubled carrier back to the right terminal half.
Equations
- Anderson4D.r324RightHalfPullback B = {i : Fin m | Anderson4D.rightMomentIndex i ∈ B}
Instances For
theorem
Anderson4D.nonemptyMomentResidualCollapseBlocks_pairwise_halfOutward
{m : ℕ}
(κp κm : PartialPairing (Fin m))
(π : ↥κp.singles ≃ ↥κm.singles)
:
The canonical nonempty residual blocks are ordered from the inner cross block to the outer blocks in both terminal half chains.
theorem
Anderson4D.r324NestedCrossSchedule_pairwise_halfOutward
{m : ℕ}
(κp κm : PartialPairing (Fin m))
(π : ↥κp.singles ≃ ↥κm.singles)
:
List.Pairwise (fun (inner outer : R324NestedCrossBlock κp κm π) => R324HalfCarrierOutward inner.carrier outer.carrier)
(r324NestedCrossSchedule κp κm π)
Enriched proof-relevant blocks retain the same outward half order.
theorem
Anderson4D.r324LeftHalfPullback_nonempty_of_crossCut
{m : ℕ}
{B : Finset (Fin (2 * m))}
(hcross : R324CrossCutCarrier m B)
:
theorem
Anderson4D.r324RightHalfPullback_nonempty_of_crossCut
{m : ℕ}
{B : Finset (Fin (2 * m))}
(hcross : R324CrossCutCarrier m B)
:
theorem
Anderson4D.leftMomentIndex_max'_r324LeftHalfPullback
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(block : R324NestedCrossBlock κp κm π)
:
The terminal left index of the canonical cross gap is the maximum of the pulled-back left carrier.
theorem
Anderson4D.rightMomentIndex_min'_r324RightHalfPullback
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(block : R324NestedCrossBlock κp κm π)
:
The terminal right index of the canonical cross gap is the minimum of the pulled-back right carrier.
theorem
Anderson4D.R324NestedCrossProperStepContext.blockOrderIso_zero_eq_min'
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
The increasing block enumeration starts at the carrier minimum.
theorem
Anderson4D.R324NestedCrossProperStepContext.blockOrderIso_last_eq_max'
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
The increasing block enumeration ends at the carrier maximum.
theorem
Anderson4D.R324NestedCrossProperStepContext.leftGapIndex_add_one_eq_rightGapIndex
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
In the increasing standard block order the two canonical gap sites are adjacent. There is no shell vertex between the last left site and the first right site.
theorem
Anderson4D.R324NestedCrossProperStepContext.leftPost_before_head
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
In the left terminal half, every post-head vertex precedes every current-head vertex.
theorem
Anderson4D.R324NestedCrossProperStepContext.rightHead_before_post
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
In the right terminal half, every current-head vertex precedes every post-head vertex.
theorem
Anderson4D.R324NestedCrossProperStepContext.leftCurrent_eq_post_union_head
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
theorem
Anderson4D.R324NestedCrossProperStepContext.rightCurrent_eq_head_union_post
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
theorem
Anderson4D.R324NestedCrossProperStepContext.leftHead_nonempty
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
theorem
Anderson4D.R324NestedCrossProperStepContext.rightHead_nonempty
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
theorem
Anderson4D.R324NestedCrossProperStepContext.leftPost_nonempty
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
theorem
Anderson4D.R324NestedCrossProperStepContext.rightPost_nonempty
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
theorem
Anderson4D.R324NestedCrossProperStepContext.leftCurrent_nonempty
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
theorem
Anderson4D.R324NestedCrossProperStepContext.rightCurrent_nonempty
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
theorem
Anderson4D.R324NestedCrossProperStepContext.leftMomentIndex_leftHead_min'
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
leftMomentIndex ((r324LeftHalfPullback ctx.step.head.carrier).min' ⋯) = ↑(ctx.step.blockOrderIso ⟨0, ⋯⟩)
The first left-half vertex of the current shell is its standard
coordinate 0.
theorem
Anderson4D.R324NestedCrossProperStepContext.rightMomentIndex_rightHead_max'
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
rightMomentIndex ((r324RightHalfPullback ctx.step.head.carrier).max' ⋯) = ↑(ctx.step.blockOrderIso (primitiveLast ctx.step.order ⋯))
The last right-half vertex of the current shell is its final standard coordinate.
theorem
Anderson4D.R324NestedCrossProperStepContext.leftMomentIndex_leftPost_max'
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
The outermost left vertex still present after the current head is the left central-gap vertex of the next literal block.
theorem
Anderson4D.R324NestedCrossProperStepContext.rightMomentIndex_rightPost_min'
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
rightMomentIndex ((r324RightHalfPullback ctx.step.next.activeCarrier).min' ⋯) = ctx.nextHead.rightGap
The innermost right vertex still present after the current head is the right central-gap vertex of the next literal block.
theorem
Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessor_internalVertex_eq_varIdx_of_no_between
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(source target : Fin m)
(htarget : target ∈ res.state.active)
(hlt : source < target)
(hnoBetween : ∀ k ∈ res.state.active, source < k → target ≤ k)
:
A local successor criterion inside the full sparse terminal chain.
Unlike edgeSuccessor_connector_eq_varIdx_min', this version does not
require the two displayed carriers to exhaust the active state: it is
enough to certify that no active vertex lies strictly between the source
and target.
theorem
Anderson4D.R324TwoHalfTerminalData.left_edgeSuccessor_connector
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
terminal.left.edgeSuccessor (r324InternalVertexEdgeSlot ((r324LeftHalfPullback ctx.step.next.activeCarrier).max' ⋯)) = varIdx ((r324LeftHalfPullback ctx.step.head.carrier).min' ⋯)
The terminal left-chain connector slot really targets the outermost left coordinate of the current shell.
theorem
Anderson4D.R324TwoHalfTerminalData.right_edgeSuccessor_connector
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
:
terminal.right.edgeSuccessor (r324InternalVertexEdgeSlot ((r324RightHalfPullback ctx.step.head.carrier).max' ⋯)) = varIdx ((r324RightHalfPullback ctx.step.next.activeCarrier).min' ⋯)
Right-chain connector successor.
theorem
Anderson4D.R324TwoHalfTerminalData.left_connector_edgeDisplacement_eq
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
(v : ctx.step.SurvivingCoordinate → T4)
:
terminal.left.edgeDisplacement 0 0
(terminal.left.reconstruct fun (i : terminal.left.SurvivingCoordinate) =>
ctx.step.reconstruct v (leftMomentIndex ↑i))
(r324InternalVertexEdgeSlot ((r324LeftHalfPullback ctx.step.next.activeCarrier).max' ⋯)) = (ctx.step.splitSurvivingPiMeasurableEquiv v).2 ctx.nextLeftPostCoordinate - (ctx.step.splitSurvivingPiMeasurableEquiv v).1 ⟨0, ⋯⟩
Coordinate identity for the left flanking leg of paper Step 3.
theorem
Anderson4D.R324TwoHalfTerminalData.right_connector_edgeDisplacement_eq
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
(v : ctx.step.SurvivingCoordinate → T4)
:
terminal.right.edgeDisplacement 0 0
(terminal.right.reconstruct fun (i : terminal.right.SurvivingCoordinate) =>
ctx.step.reconstruct v (rightMomentIndex ↑i))
(r324InternalVertexEdgeSlot ((r324RightHalfPullback ctx.step.head.carrier).max' ⋯)) = (ctx.step.splitSurvivingPiMeasurableEquiv v).1 (primitiveLast ctx.step.order ⋯) - (ctx.step.splitSurvivingPiMeasurableEquiv v).2 ctx.nextRightPostCoordinate
Coordinate identity for the right flanking leg.
noncomputable def
Anderson4D.R324TwoHalfTerminalData.leftTupleOfNestedStep
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
{π : ↥κp.singles ≃ ↥κm.singles}
(step : R324NestedCrossStepContext κp κm π)
(v : step.SurvivingCoordinate → T4)
:
terminal.left.SurvivingCoordinate → T4
Read a current nested tuple on the full terminal left carrier. Values already removed by the nested suffix are filled by its canonical zero reconstruction and never enter the current restricted slot product.
Equations
- terminal.leftTupleOfNestedStep step v i = step.reconstruct v (Anderson4D.leftMomentIndex ↑i)
Instances For
noncomputable def
Anderson4D.R324TwoHalfTerminalData.rightTupleOfNestedStep
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
{π : ↥κp.singles ≃ ↥κm.singles}
(step : R324NestedCrossStepContext κp κm π)
(v : step.SurvivingCoordinate → T4)
:
terminal.right.SurvivingCoordinate → T4
Right-half analogue.
Equations
- terminal.rightTupleOfNestedStep step v i = step.reconstruct v (Anderson4D.rightMomentIndex ↑i)
Instances For
noncomputable def
Anderson4D.R324TwoHalfTerminalData.nestedLeftHalfInvSqProduct
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
{π : ↥κp.singles ≃ ↥κm.singles}
(step : R324NestedCrossStepContext κp κm π)
(carrier : Finset (Fin (2 * m)))
(hne : (r324LeftHalfPullback carrier).Nonempty)
(v : step.SurvivingCoordinate → T4)
:
Restricted terminal left path on a doubled nested carrier.
Equations
- terminal.nestedLeftHalfInvSqProduct step carrier hne v = terminal.left.halfInvSqChainProduct (Anderson4D.r324LeftHalfPullback carrier) hne (terminal.leftTupleOfNestedStep step v)
Instances For
noncomputable def
Anderson4D.R324TwoHalfTerminalData.nestedRightHalfInvSqProduct
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
{π : ↥κp.singles ≃ ↥κm.singles}
(step : R324NestedCrossStepContext κp κm π)
(carrier : Finset (Fin (2 * m)))
(hne : (r324RightHalfPullback carrier).Nonempty)
(v : step.SurvivingCoordinate → T4)
:
Restricted terminal right path.
Equations
- terminal.nestedRightHalfInvSqProduct step carrier hne v = terminal.right.halfInvSqChainProduct (Anderson4D.r324RightHalfPullback carrier) hne (terminal.rightTupleOfNestedStep step v)
Instances For
theorem
Anderson4D.R324TwoHalfTerminalData.nestedLeftHalfInvSqProduct_current_eq
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
(v : ctx.step.SurvivingCoordinate → T4)
:
terminal.nestedLeftHalfInvSqProduct ctx.step ctx.step.residual.activeCarrier ⋯ v = terminal.nestedLeftHalfInvSqProduct ctx.step ctx.step.next.activeCarrier ⋯ v * invSqKer
(terminal.left.edgeDisplacement 0 0 (terminal.left.reconstruct (terminal.leftTupleOfNestedStep ctx.step v))
(r324InternalVertexEdgeSlot ((r324LeftHalfPullback ctx.step.next.activeCarrier).max' ⋯))) * terminal.nestedLeftHalfInvSqProduct ctx.step ctx.step.head.carrier ⋯ v
The exact left-half slot decomposition at an arbitrary proper nested step. The displayed middle factor is the unique left connector leg.
theorem
Anderson4D.R324TwoHalfTerminalData.nestedRightHalfInvSqProduct_current_eq
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
(v : ctx.step.SurvivingCoordinate → T4)
:
terminal.nestedRightHalfInvSqProduct ctx.step ctx.step.residual.activeCarrier ⋯ v = terminal.nestedRightHalfInvSqProduct ctx.step ctx.step.head.carrier ⋯ v * invSqKer
(terminal.right.edgeDisplacement 0 0 (terminal.right.reconstruct (terminal.rightTupleOfNestedStep ctx.step v))
(r324InternalVertexEdgeSlot ((r324RightHalfPullback ctx.step.head.carrier).max' ⋯))) * terminal.nestedRightHalfInvSqProduct ctx.step ctx.step.next.activeCarrier ⋯ v
Exact right-half decomposition; here the current head precedes the post carrier.
theorem
Anderson4D.R324TwoHalfTerminalData.nestedHalfInvSqProducts_current_eq_head_connector_post
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
(v : ctx.step.SurvivingCoordinate → T4)
:
terminal.nestedLeftHalfInvSqProduct ctx.step ctx.step.residual.activeCarrier ⋯ v * terminal.nestedRightHalfInvSqProduct ctx.step ctx.step.residual.activeCarrier ⋯ v = terminal.nestedLeftHalfInvSqProduct ctx.step ctx.step.head.carrier ⋯ v * terminal.nestedRightHalfInvSqProduct ctx.step ctx.step.head.carrier ⋯ v * (invSqKer
(terminal.left.edgeDisplacement 0 0 (terminal.left.reconstruct (terminal.leftTupleOfNestedStep ctx.step v))
(r324InternalVertexEdgeSlot ((r324LeftHalfPullback ctx.step.next.activeCarrier).max' ⋯))) * invSqKer
(terminal.right.edgeDisplacement 0 0 (terminal.right.reconstruct (terminal.rightTupleOfNestedStep ctx.step v))
(r324InternalVertexEdgeSlot ((r324RightHalfPullback ctx.step.head.carrier).max' ⋯)))) * (terminal.nestedLeftHalfInvSqProduct ctx.step ctx.step.next.activeCarrier ⋯ v * terminal.nestedRightHalfInvSqProduct ctx.step ctx.step.next.activeCarrier ⋯ v)
The two half paths together split as head paths, the two connector legs, and post paths. No covariance sum has been expanded.
theorem
Anderson4D.R324TwoHalfTerminalData.nestedHalfInvSqProducts_current_eq_head_connector_post_named
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossProperStepContext κp κm π)
(v : ctx.step.SurvivingCoordinate → T4)
:
terminal.nestedLeftHalfInvSqProduct ctx.step ctx.step.residual.activeCarrier ⋯ v * terminal.nestedRightHalfInvSqProduct ctx.step ctx.step.residual.activeCarrier ⋯ v = terminal.nestedLeftHalfInvSqProduct ctx.step ctx.step.head.carrier ⋯ v * terminal.nestedRightHalfInvSqProduct ctx.step ctx.step.head.carrier ⋯ v * ctx.connector (ctx.step.splitSurvivingPiMeasurableEquiv v).1 (ctx.step.splitSurvivingPiMeasurableEquiv v).2 * (terminal.nestedLeftHalfInvSqProduct ctx.step ctx.step.next.activeCarrier ⋯ v * terminal.nestedRightHalfInvSqProduct ctx.step ctx.step.next.activeCarrier ⋯ v)
Paper Step 3 chain geometry in its exact named form: the two current
terminal half paths split into the current shell paths, ctx.connector's
two flanking legs, and the unchanged post-shell paths.