Geometry of the R-322 analytic schedule

The right-endpoint sort is useful only after reconnecting every scheduled endpoint pair with the laminar extraction geometry. This file proves that an earlier scheduled interval is either strictly to the left of a later one, or is strictly contained in it. These are precisely the two geometric branches that support the paper's inside-to-outside analytic collapse.

def Anderson4D.R322PaperEarlier {m : ℕ} (p q : Fin m × Fin m) : Prop

Paper-order geometry: the earlier interval is either strictly to the left of the later interval, or strictly contained in it.

Equations

• Anderson4D.R322PaperEarlier p q = (p.2 < q.1 ∨ q.1 < p.1 ∧ p.2 < q.2)

Returning scheduled endpoints to the extraction list

theorem Anderson4D.r322AnalyticSchedule_endpoint_mem_extract {m : ℕ} (κ : PartialPairing (Fin m)) {s : R322ExtractionStep m} (hs : s ∈ r322AnalyticSchedule κ) : s.1 ∈ extract κ

Every endpoint pair appearing in the analytic schedule still belongs to the original extraction list.

theorem Anderson4D.r322AnalyticSchedule_get_endpoint_mem_extract {m : ℕ} (κ : PartialPairing (Fin m)) (i : Fin (r322AnalyticSchedule κ).length) : ((r322AnalyticSchedule κ).get i).1 ∈ extract κ

Endpoint membership specialized to a list index.

theorem Anderson4D.r322AnalyticSchedule_get_endpoints_mem_extract {m : ℕ} (κ : PartialPairing (Fin m)) (i j : Fin (r322AnalyticSchedule κ).length) : ((r322AnalyticSchedule κ).get i).1 ∈ extract κ ∧ ((r322AnalyticSchedule κ).get j).1 ∈ extract κ

Both endpoint pairs at two schedule indices belong to the original extraction list.

Indexed strict order

theorem Anderson4D.r322AnalyticSchedule_get_right_lt {m : ℕ} (κ : PartialPairing (Fin m)) {i j : Fin (r322AnalyticSchedule κ).length} (hij : i < j) : ((r322AnalyticSchedule κ).get i).1.2 < ((r322AnalyticSchedule κ).get j).1.2

Any earlier list index has a strictly smaller right endpoint.

Laminarity independent of the selector's original list order

theorem Anderson4D.extract_laminar_of_mem_of_ne' {m : ℕ} {κ : PartialPairing (Fin m)} {p q : Fin m × Fin m} (hp : p ∈ extract κ) (hq : q ∈ extract κ) (hpq : p ≠ q) : ReductionIntervalsLaminar p q

Two distinct members of the extraction list are laminar, independently of which one occurred first in the selector recursion.

theorem Anderson4D.r322AnalyticSchedule_pairwise_laminar {m : ℕ} (κ : PartialPairing (Fin m)) : List.Pairwise (fun (s t : R322ExtractionStep m) => ReductionIntervalsLaminar s.1 t.1) (r322AnalyticSchedule κ)

Scheduled endpoint intervals are pairwise laminar.

The two admissible paper-order branches

theorem Anderson4D.r322AnalyticSchedule_pairwise_paperEarlier {m : ℕ} (κ : PartialPairing (Fin m)) : List.Pairwise (fun (s t : R322ExtractionStep m) => R322PaperEarlier s.1 t.1) (r322AnalyticSchedule κ)

Combining laminarity with increasing right endpoints eliminates the two geometrically impossible branches.

theorem Anderson4D.r322AnalyticSchedule_get_paperEarlier {m : ℕ} (κ : PartialPairing (Fin m)) {i j : Fin (r322AnalyticSchedule κ).length} (hij : i < j) : R322PaperEarlier ((r322AnalyticSchedule κ).get i).1 ((r322AnalyticSchedule κ).get j).1

Indexed form of the paper-order geometry.

theorem Anderson4D.r322AnalyticSchedule_head_later_right_or_contains {m : ℕ} (κ : PartialPairing (Fin m)) {head : R322ExtractionStep m} {tail : List (R322ExtractionStep m)} (hschedule : r322AnalyticSchedule κ = head :: tail) {later : R322ExtractionStep m} (hlater : later ∈ tail) : head.1.2 < later.1.1 ∨ later.1.1 < head.1.1 ∧ head.1.2 < later.1.2

Head/tail form consumed by an inside-to-outside collapse induction.