Moving the genuine first-left selector block into analytic position

The first-left R-324 fibre is indexed by the first block chosen by selectRel. The R-322 analytic collapse instead sorts all extraction steps by increasing right endpoint. Those blocks need not be literally the same list head: analytic steps preceding the selector block can be disjoint from it.

This file closes that representation-order discrepancy. It locates the actual first-left selector step in the analytic schedule, moves it to the front by an explicit list permutation, and proves that every crossed block is disjoint from the selected coordinates occurring in R324FirstLeftPhysicalRouting.

The selector step inside the analytic schedule

def Anderson4D.r324FirstLeftSelectedStep {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : R322ExtractionStep m

The endpoint/block pair selected by the genuine first left reduction step of the R-324 fibre.

Equations

• Anderson4D.r324FirstLeftSelectedStep e₀ hleft = (Anderson4D.selectRel e₀.fst Finset.univ hleft, Anderson4D.selectedExtractionBlock e₀.fst Finset.univ hleft)

@[simp]

theorem Anderson4D.r324FirstLeftSelectedStep_endpoint {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : (r324FirstLeftSelectedStep e₀ hleft).1 = selectRel e₀.fst Finset.univ hleft

@[simp]

theorem Anderson4D.r324FirstLeftSelectedStep_block {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : (r324FirstLeftSelectedStep e₀ hleft).2 = selectedExtractionBlock e₀.fst Finset.univ hleft

theorem Anderson4D.r324FirstLeftSelectedStep_mem_extractionTrace {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : r324FirstLeftSelectedStep e₀ hleft ∈ (extract e₀.fst).zip (extractionBlocks e₀.fst)

The genuine selector step occurs in the unsorted aligned extraction trace. This is the point where both its endpoint pair and its concrete block are tied back to the original reduction recursion.

theorem Anderson4D.r324FirstLeftSelectedStep_mem_analyticSchedule {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : r324FirstLeftSelectedStep e₀ hleft ∈ r322AnalyticSchedule e₀.fst

Hence the genuine selector step also occurs in the right-endpoint sorted analytic schedule.

Explicitly commuting the disjoint analytic prefix

theorem Anderson4D.exists_r324FirstLeft_analytic_decomposition {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : ∃ (pre : List (R322ExtractionStep m)) (post : List (R322ExtractionStep m)), r322AnalyticSchedule e₀.fst = pre ++ r324FirstLeftSelectedStep e₀ hleft :: post ∧ ∀ earlier ∈ pre, Disjoint earlier.2 (selectedExtractionBlock e₀.fst Finset.univ hleft)

Exact schedule decomposition at the genuine first-left selector step. Every analytic step which the selector step crosses is spatially disjoint from it.

theorem Anderson4D.r324FirstLeft_analytic_reorder {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : ∃ (pre : List (R322ExtractionStep m)) (post : List (R322ExtractionStep m)), r322AnalyticSchedule e₀.fst = pre ++ r324FirstLeftSelectedStep e₀ hleft :: post ∧ (r322AnalyticSchedule e₀.fst).Perm (r324FirstLeftSelectedStep e₀ hleft :: (pre ++ post)) ∧ (∀ earlier ∈ pre, Disjoint (Finset.image leftMomentIndex earlier.2) (Finset.image leftMomentIndex (selectedExtractionBlock e₀.fst Finset.univ hleft))) ∧ selectedExtractionBlock e₀.fst Finset.univ hleft = r322AnalyticActiveCarrier pre ∩ Finset.Icc (selectRel e₀.fst Finset.univ hleft).1 (selectRel e₀.fst Finset.univ hleft).2

Selector/analytic-order bridge.

The actual first-left selector step may be moved to the head of the analytic list. The permutation crosses only disjoint blocks, and those crossed blocks remain completely outside the doubled spatial-coordinate set integrated on the inside by integral_sum_deterministicMomentIntegrand_eq_firstLeft_primitive.