Documentation

Anderson4D.DetParametrix.Paper41_Renorm.R322AnalyticScheduleTerminal

Terminal structure of the R-322 analytic schedule #

For a non-splitting full pairing, the whole-interval endpoint pair occurs in the extraction list. It cannot precede any other interval in paper order, so the analytic schedule consists of a (possibly empty) proper prefix followed by one terminal step with that endpoint pair. The terminal step's concrete block is intentionally left unspecified: it is the residual trace after the proper collapses, not the original full carrier.

source
def Anderson4D.r322WholeEndpoint (q : ℕ) (hq : 1 ≤ q) :
Fin (2 * q) × Fin (2 * q)

The endpoint pair spanning the full carrier of a nonempty pairing.

Equations
Instances For
    source
    theorem Anderson4D.r322WholeEndpoint_not_paperEarlier (q : ℕ) (hq : 1 ≤ q) (p : Fin (2 * q) × Fin (2 * q)) :
    ¬R322PaperEarlier (r322WholeEndpoint q hq) p

    A whole-interval endpoint cannot occur before another interval in the paper's analytic order.

    Proper-prefix / terminal decomposition #

    source
    theorem Anderson4D.r322AnalyticSchedule_eq_proper_append_terminal_of_isNonSplit {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hq : 1 ≤ q) (hκ : IsNonSplit κ) :
    ∃ (proper : List (R322ExtractionStep (2 * q))) (terminal : R322ExtractionStep (2 * q)), r322AnalyticSchedule κ = proper ++ [terminal] ∧ terminal.1 = r322WholeEndpoint q hq ∧ ∀ s ∈ proper, s.1 ≠ r322WholeEndpoint q hq

    A non-splitting analytic schedule is a proper prefix followed by a step whose endpoint is the whole interval. No prefix endpoint is the whole interval.

    Head/tail interface for the collapse induction #

    source
    theorem Anderson4D.r322AnalyticSchedule_head_proper_or_terminal {q : ℕ} {κ : PartialPairing (Fin (2 * q))} (hq : 1 ≤ q) (hκ : IsNonSplit κ) {head : R322ExtractionStep (2 * q)} {tail : List (R322ExtractionStep (2 * q))} (hschedule : r322AnalyticSchedule κ = head :: tail) :
    tail = [] ∧ head.1 = r322WholeEndpoint q hq ∨ tail ≠ [] ∧ head.1 ≠ r322WholeEndpoint q hq

    At the head of a non-splitting schedule, an empty tail means that the head is the terminal whole-interval step; a nonempty tail means that the head is proper.