The analytic prefix step carrying the R-324 predecessor #
If the production predecessor edge of the first-left block is extracted, its generating analytic step is the last step before the selected block. This is a statement about the genuine schedule and disjoint extraction blocks, not a pointwise identity between pre- and post-collapse edges.
theorem
Anderson4D.r324FirstLeft_extractedPredecessor_adjacent
{m : ℕ}
(e₀ : MomentContraction m)
(hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b)
(step : R322ExtractionStep m)
(hedge : extractedRightEdge step.1 = r324FirstLeftPredecessorEdge e₀ hleft)
:
Equality of extracted edge slots says exactly that the prefix block ends immediately before the selected first-left block begins.
theorem
Anderson4D.r324FirstLeft_prefixPredecessor_is_last
{m : ℕ}
(e₀ : MomentContraction m)
(hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b)
(pre post : List (R322ExtractionStep m))
(step : R322ExtractionStep m)
(hschedule : r322AnalyticSchedule e₀.fst = pre ++ r324FirstLeftSelectedStep e₀ hleft :: post)
(hstep : step ∈ pre)
(hedge : extractedRightEdge step.1 = r324FirstLeftPredecessorEdge e₀ hleft)
:
No scheduled block can occur between the block producing the selected predecessor and the selected block itself.
theorem
Anderson4D.exists_r324FirstLeft_lastAnalyticPredecessor
{m : ℕ}
(e₀ : MomentContraction m)
(hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b)
(hextracted : r324FirstLeftPredecessorEdge e₀ hleft ∈ extractedRightEdges e₀.fst)
:
∃ (prior : List (R322ExtractionStep m)) (step : R322ExtractionStep m) (post : List (R322ExtractionStep m)),
r322AnalyticSchedule e₀.fst = prior ++ [step] ++ r324FirstLeftSelectedStep e₀ hleft :: post ∧ extractedRightEdge step.1 = r324FirstLeftPredecessorEdge e₀ hleft ∧ ↑step.1.2 + 1 = ↑(r324FirstLeftSelectedStep e₀ hleft).1.1
Canonical decomposition at the extracted predecessor: the last prefix step is adjacent to the selected first-left block.