Documentation

Anderson4D.DetParametrix.Paper42_Moment.R324PaperTraceExteriorParts

Cross-cut trace and exterior parts #

The shell calculation has two endpoint analogues. A cross-cut trace is a terminal interval in each half of the active order, while the exterior is the complementary initial or terminal interval. These identities provide the first and last blocks in the paper's Step 3 chain decomposition.

source
theorem Anderson4D.residualIntervalTrace_filter_lt {n m : ℕ} (active : Finset (Fin n)) (p : Fin n × Fin n) (hmp2 : m ≤ ↑p.2) :
{i ∈ residualIntervalTrace active p | ↑i < m} = {i ∈ active | p.1 ≤ i ∧ ↑i < m}

Below the cut, a straddling trace is the relative interval starting at its left endpoint and ending just before the cut.

source
theorem Anderson4D.residualIntervalTrace_filter_ge {n m : ℕ} (active : Finset (Fin n)) (p : Fin n × Fin n) (hp1 : ↑p.1 < m) :
{i ∈ residualIntervalTrace active p | m ≤ ↑i} = {i ∈ active | m ≤ ↑i ∧ i ≤ p.2}

Above the cut, a straddling trace is the relative interval from the cut through its right endpoint.

source
theorem Anderson4D.residualIntervalExterior_filter_lt {n m : ℕ} (active : Finset (Fin n)) (p : Fin n × Fin n) (hp1 : ↑p.1 < m) (hmp2 : m ≤ ↑p.2) :
{i ∈ residualIntervalExterior active p | ↑i < m} = {i ∈ active | i < p.1}

Below the cut, the exterior of a straddling interval is exactly the active initial interval strictly before its left endpoint.

source
theorem Anderson4D.residualIntervalExterior_filter_ge {n m : ℕ} (active : Finset (Fin n)) (p : Fin n × Fin n) (hp1 : ↑p.1 < m) (hmp2 : m ≤ ↑p.2) :
{i ∈ residualIntervalExterior active p | m ≤ ↑i} = {i ∈ active | p.2 < i}

Above the cut, the exterior is exactly the active terminal interval strictly after the right endpoint.

Contiguity in the relative active order #

source
def Anderson4D.FinsetOrdConnectedWithin {n : ℕ} (active part : Finset (Fin n)) :
Prop

A finite part is contiguous relative to active when its pullback to the linearly ordered subtype of active vertices is order-connected. This is the standard Set.OrdConnected predicate, applied to the relative carrier rather than to the ambient Fin n (where gaps in active are intentional).

Equations
Instances For
    source
    theorem Anderson4D.residualIntervalTrace_filter_lt_ordConnectedWithin {n m : ℕ} (active : Finset (Fin n)) (p : Fin n × Fin n) (hmp2 : m ≤ ↑p.2) :
    FinsetOrdConnectedWithin active ({i ∈ residualIntervalTrace active p | ↑i < m})

    The below-cut trace is contiguous in the active order.

    source
    theorem Anderson4D.residualIntervalTrace_filter_ge_ordConnectedWithin {n m : ℕ} (active : Finset (Fin n)) (p : Fin n × Fin n) (hp1 : ↑p.1 < m) :
    FinsetOrdConnectedWithin active ({i ∈ residualIntervalTrace active p | m ≤ ↑i})

    The above-cut trace is contiguous in the active order.

    source
    theorem Anderson4D.residualIntervalExterior_filter_lt_ordConnectedWithin {n m : ℕ} (active : Finset (Fin n)) (p : Fin n × Fin n) (hp1 : ↑p.1 < m) (hmp2 : m ≤ ↑p.2) :
    FinsetOrdConnectedWithin active ({i ∈ residualIntervalExterior active p | ↑i < m})

    The below-cut exterior is contiguous in the active order.

    source
    theorem Anderson4D.residualIntervalExterior_filter_ge_ordConnectedWithin {n m : ℕ} (active : Finset (Fin n)) (p : Fin n × Fin n) (hp1 : ↑p.1 < m) (hmp2 : m ≤ ↑p.2) :
    FinsetOrdConnectedWithin active ({i ∈ residualIntervalExterior active p | m ≤ ↑i})

    The above-cut exterior is contiguous in the active order.