The analytic schedule for R-322

The closed-form extraction list records the deterministic selector from the combinatorial recursion. The analytic collapse, however, must process a primitive interval before every interval that contains it. Since extraction intervals are laminar, sorting the aligned endpoint/block steps by increasing right endpoint gives exactly such an inside-to-outside schedule; disjoint intervals may be interchanged.

@[reducible, inline]

abbrev Anderson4D.R322ExtractionStep (m : ℕ) : Type

An extraction endpoint together with the concrete trace removed at the same recursive step.

Equations

• Anderson4D.R322ExtractionStep m = ((Fin m × Fin m) × Finset (Fin m))

def Anderson4D.R322StepRightLE {m : ℕ} (s t : R322ExtractionStep m) : Prop

The weak right-endpoint order used by insertion sort. Right endpoints of distinct extracted intervals are in fact distinct, so the resulting schedule is strictly ordered.

Equations

• Anderson4D.R322StepRightLE s t = (s.1.2 ≤ t.1.2)

@[implicit_reducible]

instance Anderson4D.instDecidableRelR322ExtractionStepR322StepRightLE {m : ℕ} : DecidableRel R322StepRightLE

Equations

• Anderson4D.instDecidableRelR322ExtractionStepR322StepRightLE x✝¹ x✝ = Anderson4D.instDecidableRelR322ExtractionStepR322StepRightLE._aux_1 x✝¹ x✝

instance Anderson4D.instTotalR322ExtractionStepR322StepRightLE {m : ℕ} : Std.Total R322StepRightLE

instance Anderson4D.instIsTransR322ExtractionStepR322StepRightLE {m : ℕ} : IsTrans (R322ExtractionStep m) R322StepRightLE

def Anderson4D.r322AnalyticSchedule {m : ℕ} (κ : PartialPairing (Fin m)) : List (R322ExtractionStep m)

The endpoint/block extraction trace, reordered into the analytic inside-to-outside schedule.

Equations

• Anderson4D.r322AnalyticSchedule κ = List.insertionSort Anderson4D.R322StepRightLE ((Anderson4D.extract κ).zip (Anderson4D.extractionBlocks κ))

theorem Anderson4D.r322AnalyticSchedule_endpoints_perm_extract {m : ℕ} (κ : PartialPairing (Fin m)) : (List.map Prod.fst (r322AnalyticSchedule κ)).Perm (extract κ)

Projection of the analytic schedule to endpoint pairs is a permutation of the public extraction list.

theorem Anderson4D.r322AnalyticSchedule_blocks_perm_extractionBlocks {m : ℕ} (κ : PartialPairing (Fin m)) : (List.map Prod.snd (r322AnalyticSchedule κ)).Perm (extractionBlocks κ)

Projection of the analytic schedule to concrete blocks is a permutation of the public extraction-block list.

theorem Anderson4D.r322AnalyticSchedule_forall_aligned {m : ℕ} (κ : PartialPairing (Fin m)) (s : R322ExtractionStep m) : s ∈ r322AnalyticSchedule κ → ExtractionPairBlockAligned s.1 s.2

Sorting retains the pointwise endpoint/block alignment proved for the original recursion.

Strict right-endpoint order

theorem Anderson4D.r322AnalyticSchedule_pairwise_right_le {m : ℕ} (κ : PartialPairing (Fin m)) : List.Pairwise R322StepRightLE (r322AnalyticSchedule κ)

Insertion sort puts the analytic schedule in weakly increasing right-endpoint order.

theorem Anderson4D.r322AnalyticSchedule_rightEndpoints_nodup {m : ℕ} (κ : PartialPairing (Fin m)) : (List.map (fun (s : R322ExtractionStep m) => s.1.2) (r322AnalyticSchedule κ)).Nodup

The schedule has no repeated right endpoints.

theorem Anderson4D.r322AnalyticSchedule_pairwise_right_lt {m : ℕ} (κ : PartialPairing (Fin m)) : List.Pairwise (fun (s t : R322ExtractionStep m) => s.1.2 < t.1.2) (r322AnalyticSchedule κ)

Right endpoints in analytic execution order are strictly increasing.