Documentation

Anderson4D.DetParametrix.Paper42_Moment.R324ShortcutTerminalSchedule

Terminal schedule for the R-324 outgoing-shortcut branch #

If the final chain edge belongs to the extracted-edge set of a partial pairing, the strict right-endpoint order on the analytic schedule forces its unique corresponding extraction step to be last. This file packages that proper-prefix/terminal decomposition without assuming that the pairing is full. In particular, it deliberately records no claim that the terminal block exhausts the active carrier.

source
structure Anderson4D.R324ShortcutTerminalSchedule {m : ℕ} (κ : PartialPairing (Fin m)) :
Type

The proper-prefix/terminal decomposition of an analytic schedule whose final extracted right edge is the outgoing chain edge.

Instances For
    source
    theorem Anderson4D.R324ShortcutTerminalSchedule.terminal_right {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324ShortcutTerminalSchedule κ) :
    ↑data.terminal.1.2 = m - 1

    The right endpoint of the terminal extracted interval is the final internal vertex.

    source
    theorem Anderson4D.R324ShortcutTerminalSchedule.terminal_mem_schedule {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324ShortcutTerminalSchedule κ) :
    data.terminal ∈ r322AnalyticSchedule κ

    The distinguished terminal step occurs in the analytic schedule.

    source
    theorem Anderson4D.R324ShortcutTerminalSchedule.mem_schedule_of_mem_proper {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324ShortcutTerminalSchedule κ) {step : R322ExtractionStep m} (hstep : step ∈ data.proper) :
    step ∈ r322AnalyticSchedule κ

    Every step in the proper prefix occurs in the analytic schedule.

    source
    theorem Anderson4D.R324ShortcutTerminalSchedule.terminal_endpoint_mem_extract {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324ShortcutTerminalSchedule κ) :
    data.terminal.1 ∈ extract κ

    The endpoint pair of the terminal step belongs to the extraction list.

    source
    theorem Anderson4D.R324ShortcutTerminalSchedule.proper_endpoint_mem_extract {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324ShortcutTerminalSchedule κ) {step : R322ExtractionStep m} (hstep : step ∈ data.proper) :
    step.1 ∈ extract κ

    Every endpoint pair in the proper prefix belongs to the extraction list.

    source
    theorem Anderson4D.R324ShortcutTerminalSchedule.last_mem_extractedRightEdges {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324ShortcutTerminalSchedule κ) :
    Fin.last m ∈ extractedRightEdges κ

    The outgoing edge is indeed present in the extracted-edge set.

    source
    theorem Anderson4D.R324ShortcutTerminalSchedule.proper_extractedRightEdge_ne_last {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324ShortcutTerminalSchedule κ) (step : R322ExtractionStep m) (hstep : step ∈ data.proper) :
    extractedRightEdge step.1 ≠ Fin.last m

    No step in the proper prefix extracts the outgoing chain edge.

    source
    theorem Anderson4D.R324ShortcutTerminalSchedule.eq_terminal_of_mem_schedule_of_extractedRightEdge_eq_last {m : ℕ} {κ : PartialPairing (Fin m)} (data : R324ShortcutTerminalSchedule κ) (step : R322ExtractionStep m) (hstep : step ∈ r322AnalyticSchedule κ) (hedge : extractedRightEdge step.1 = Fin.last m) :
    step = data.terminal

    The distinguished terminal is the unique scheduled step extracting the outgoing chain edge.

    source
    theorem Anderson4D.R324ShortcutTerminalSchedule.unique {m : ℕ} {κ : PartialPairing (Fin m)} (left right : R324ShortcutTerminalSchedule κ) :
    left = right

    The proper-prefix/terminal decomposition is unique.

    source
    theorem Anderson4D.exists_r324ShortcutTerminalSchedule {m : ℕ} (κ : PartialPairing (Fin m)) (hshortcut : Fin.last m ∈ extractedRightEdges κ) :
    Nonempty (R324ShortcutTerminalSchedule κ)

    If the outgoing chain edge is extracted, strict schedule order produces the canonical terminal decomposition without any fullness assumption.

    source
    theorem Anderson4D.existsUnique_r324ShortcutTerminalStep {m : ℕ} (κ : PartialPairing (Fin m)) (hshortcut : Fin.last m ∈ extractedRightEdges κ) :
    ∃! terminal : R322ExtractionStep m, terminal ∈ r322AnalyticSchedule κ ∧ extractedRightEdge terminal.1 = Fin.last m

    There is exactly one scheduled step whose extracted right edge is the outgoing chain edge.