Ordered half-chain partitions for the paper's nested Step 3 #
The endpoint-erased chain of a completed half has one slot for every surviving vertex except the last one. If a current carrier is split into two nonempty consecutive pieces, those slots split into the internal slots of the first piece, the unique slot at its last vertex, and the internal slots of the second piece. The middle slot is the flanking connector used by the nested-cross induction.
def
Anderson4D.R324WithinHalfResidualPrefix.halfChainEdgeSlots
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(_res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(carrier : Finset (Fin m))
(hne : carrier.Nonempty)
:
Production slots of a nonempty sparse half-carrier, with its terminal source vertex erased.
Equations
- _res.halfChainEdgeSlots carrier hne = Finset.image Anderson4D.r324InternalVertexEdgeSlot (carrier.erase (carrier.max' hne))
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.endpointErasedActiveEdgeSlots_eq_halfChainEdgeSlots
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(hactive : res.state.active.Nonempty)
:
The endpoint-erased active slots are exactly the nonterminal source slots of the full surviving half-carrier.
def
Anderson4D.R324WithinHalfResidualPrefix.HalfCarrierBefore
{m : ℕ}
(first second : Finset (Fin m))
:
Strict separation of two finite half-carriers.
Equations
- Anderson4D.R324WithinHalfResidualPrefix.HalfCarrierBefore first second = ∀ i ∈ first, ∀ j ∈ second, i < j
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.halfChainEdgeSlots_union_eq_threeWay_of_before
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(first second : Finset (Fin m))
(hfirst : first.Nonempty)
(hsecond : second.Nonempty)
(hbefore : HalfCarrierBefore first second)
:
res.halfChainEdgeSlots (first ∪ second) ⋯ = res.halfChainEdgeSlots first hfirst ∪ {r324InternalVertexEdgeSlot (first.max' hfirst)} ∪ res.halfChainEdgeSlots second hsecond
Three-way ordered slot partition. For consecutive nonempty
carriers first < second, the only slot between their two internal paths
is the slot sourced at max first.
theorem
Anderson4D.R324WithinHalfResidualPrefix.halfChainEdgeSlots_disjoint_connector
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(carrier : Finset (Fin m))
(hne : carrier.Nonempty)
:
Disjoint (res.halfChainEdgeSlots carrier hne) {r324InternalVertexEdgeSlot (carrier.max' hne)}
The first internal slot family is disjoint from its outgoing connector.
theorem
Anderson4D.R324WithinHalfResidualPrefix.halfChainEdgeSlots_disjoint_of_before
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(first second : Finset (Fin m))
(hfirst : first.Nonempty)
(hsecond : second.Nonempty)
(hbefore : HalfCarrierBefore first second)
:
Disjoint (res.halfChainEdgeSlots first hfirst) (res.halfChainEdgeSlots second hsecond)
All slots belonging to strictly separated carriers are disjoint.
theorem
Anderson4D.R324WithinHalfResidualPrefix.connector_disjoint_halfChainEdgeSlots_of_before
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(first second : Finset (Fin m))
(hfirst : first.Nonempty)
(hsecond : second.Nonempty)
(hbefore : HalfCarrierBefore first second)
:
Disjoint {r324InternalVertexEdgeSlot (first.max' hfirst)} (res.halfChainEdgeSlots second hsecond)
The connector slot is disjoint from every slot in the later carrier.
theorem
Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessor_connector_eq_varIdx_min'
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(first second : Finset (Fin m))
(hfirst : first.Nonempty)
(hsecond : second.Nonempty)
(hbefore : HalfCarrierBefore first second)
(hactive : res.state.active = first ∪ second)
:
When the two consecutive pieces exhaust the active carrier, the successor of the unique connector source is the first vertex of the later piece. This identifies the singleton slot above with the literal sparse chain leg, not merely with a counting placeholder.
theorem
Anderson4D.R324WithinHalfResidualPrefix.edgeDisplacement_connector_eq
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(first second : Finset (Fin m))
(hfirst : first.Nonempty)
(hsecond : second.Nonempty)
(hbefore : HalfCarrierBefore first second)
(hactive : res.state.active = first ∪ second)
(v : res.SurvivingCoordinate → T4)
:
res.edgeDisplacement 0 0 (res.reconstruct v) (r324InternalVertexEdgeSlot (first.max' hfirst)) = v ⟨first.max' hfirst, ⋯⟩ - v ⟨second.min' hsecond, ⋯⟩
Coordinate form of the connector leg.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.halfInvSqChainProduct
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(carrier : Finset (Fin m))
(hne : carrier.Nonempty)
(v : res.SurvivingCoordinate → T4)
:
Inverse-square product restricted to one nonempty half-carrier.
Equations
- res.halfInvSqChainProduct carrier hne v = ∏ edge ∈ res.halfChainEdgeSlots carrier hne, Anderson4D.invSqKer (res.edgeDisplacement 0 0 (res.reconstruct v) edge)
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.endpointErasedInvSqChainProduct_eq_halfInvSqChainProduct
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(hactive : res.state.active.Nonempty)
(v : res.SurvivingCoordinate → T4)
:
res.endpointErasedInvSqChainProduct hactive v = res.halfInvSqChainProduct res.state.active hactive v
The full endpoint-erased inverse-square chain is the restricted product on the complete active carrier.
theorem
Anderson4D.R324WithinHalfResidualPrefix.halfInvSqChainProduct_union_eq_threeWay_of_before
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(first second : Finset (Fin m))
(hfirst : first.Nonempty)
(hsecond : second.Nonempty)
(hbefore : HalfCarrierBefore first second)
(v : res.SurvivingCoordinate → T4)
:
res.halfInvSqChainProduct (first ∪ second) ⋯ v = res.halfInvSqChainProduct first hfirst v * invSqKer (res.edgeDisplacement 0 0 (res.reconstruct v) (r324InternalVertexEdgeSlot (first.max' hfirst))) * res.halfInvSqChainProduct second hsecond v
Product form of the three-way ordered slot partition.
Canonical initial/terminal interval specializations #
def
Anderson4D.R324WithinHalfResidualPrefix.halfCarrierBeforeCut
{m : ℕ}
(carrier : Finset (Fin m))
(cut : Fin m)
:
The part of a half-carrier strictly before a cut vertex.
Equations
- Anderson4D.R324WithinHalfResidualPrefix.halfCarrierBeforeCut carrier cut = {i ∈ carrier | i < cut}
Instances For
def
Anderson4D.R324WithinHalfResidualPrefix.halfCarrierFromCut
{m : ℕ}
(carrier : Finset (Fin m))
(cut : Fin m)
:
The part of a half-carrier at or after a cut vertex.
Equations
- Anderson4D.R324WithinHalfResidualPrefix.halfCarrierFromCut carrier cut = {i ∈ carrier | cut ≤ i}
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.halfCarrierBeforeCut_union_fromCut
{m : ℕ}
(carrier : Finset (Fin m))
(cut : Fin m)
:
theorem
Anderson4D.R324WithinHalfResidualPrefix.halfCarrierBefore_before_fromCut
{m : ℕ}
(carrier : Finset (Fin m))
(cut : Fin m)
:
HalfCarrierBefore (halfCarrierBeforeCut carrier cut) (halfCarrierFromCut carrier cut)
theorem
Anderson4D.R324WithinHalfResidualPrefix.halfInvSqChainProduct_eq_post_connector_head
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(carrier : Finset (Fin m))
(cut : Fin m)
(hpost : (halfCarrierBeforeCut carrier cut).Nonempty)
(hhead : (halfCarrierFromCut carrier cut).Nonempty)
(v : res.SurvivingCoordinate → T4)
:
res.halfInvSqChainProduct carrier ⋯ v = res.halfInvSqChainProduct (halfCarrierBeforeCut carrier cut) hpost v * invSqKer
(res.edgeDisplacement 0 0 (res.reconstruct v)
(r324InternalVertexEdgeSlot ((halfCarrierBeforeCut carrier cut).max' hpost))) * res.halfInvSqChainProduct (halfCarrierFromCut carrier cut) hhead v
Left-half orientation: the post-carrier is before the current head. Its greatest source slot is the unique connector into the head.
def
Anderson4D.R324WithinHalfResidualPrefix.halfCarrierThroughCut
{m : ℕ}
(carrier : Finset (Fin m))
(cut : Fin m)
:
The part of a half-carrier through a terminal cut vertex.
Equations
- Anderson4D.R324WithinHalfResidualPrefix.halfCarrierThroughCut carrier cut = {i ∈ carrier | i ≤ cut}
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.halfCarrierThroughCut_union_afterCut
{m : ℕ}
(carrier : Finset (Fin m))
(cut : Fin m)
:
theorem
Anderson4D.R324WithinHalfResidualPrefix.halfCarrierThrough_before_afterCut
{m : ℕ}
(carrier : Finset (Fin m))
(cut : Fin m)
:
HalfCarrierBefore (halfCarrierThroughCut carrier cut) (halfCarrierAfterCut carrier cut)
theorem
Anderson4D.R324WithinHalfResidualPrefix.halfInvSqChainProduct_eq_head_connector_post
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(carrier : Finset (Fin m))
(cut : Fin m)
(hhead : (halfCarrierThroughCut carrier cut).Nonempty)
(hpost : (halfCarrierAfterCut carrier cut).Nonempty)
(v : res.SurvivingCoordinate → T4)
:
res.halfInvSqChainProduct carrier ⋯ v = res.halfInvSqChainProduct (halfCarrierThroughCut carrier cut) hhead v * invSqKer
(res.edgeDisplacement 0 0 (res.reconstruct v)
(r324InternalVertexEdgeSlot ((halfCarrierThroughCut carrier cut).max' hhead))) * res.halfInvSqChainProduct (halfCarrierAfterCut carrier cut) hpost v
Right-half orientation: the current head precedes the post-carrier. The slot at the head maximum is the unique connector into the post path.
theorem
Anderson4D.R324WithinHalfResidualPrefix.endpointErasedInvSqChainProduct_eq_post_connector_head
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(hactive : res.state.active.Nonempty)
(cut : Fin m)
(hpost : (halfCarrierBeforeCut res.state.active cut).Nonempty)
(hhead : (halfCarrierFromCut res.state.active cut).Nonempty)
(v : res.SurvivingCoordinate → T4)
:
res.endpointErasedInvSqChainProduct hactive v = res.halfInvSqChainProduct (halfCarrierBeforeCut res.state.active cut) hpost v * invSqKer
(res.edgeDisplacement 0 0 (res.reconstruct v)
(r324InternalVertexEdgeSlot ((halfCarrierBeforeCut res.state.active cut).max' hpost))) * res.halfInvSqChainProduct (halfCarrierFromCut res.state.active cut) hhead v
Full terminal left-half specialization, stated directly for the paper's endpoint-erased chain.
theorem
Anderson4D.R324WithinHalfResidualPrefix.endpointErasedInvSqChainProduct_eq_head_connector_post
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(hactive : res.state.active.Nonempty)
(cut : Fin m)
(hhead : (halfCarrierThroughCut res.state.active cut).Nonempty)
(hpost : (halfCarrierAfterCut res.state.active cut).Nonempty)
(v : res.SurvivingCoordinate → T4)
:
res.endpointErasedInvSqChainProduct hactive v = res.halfInvSqChainProduct (halfCarrierThroughCut res.state.active cut) hhead v * invSqKer
(res.edgeDisplacement 0 0 (res.reconstruct v)
(r324InternalVertexEdgeSlot ((halfCarrierThroughCut res.state.active cut).max' hhead))) * res.halfInvSqChainProduct (halfCarrierAfterCut res.state.active cut) hpost v
Full terminal right-half specialization.