Imports
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorTransitionStatementStackRouteCount
import Mathlib.Data.Fin.Tuple.TakeSemantic prefix selected by terminal stack route counts
The concrete descriptor pass changes a progression count from n to
n - c. This file records the corresponding value-level fact: it selects
exactly that prefix of the original affine source stream.
noncomputable sectionnamespace CLRS.Chapter34.Turing.CookLevinopen PolyBuilderSaturating count subtraction is exactly prefix selection on the rows generated by an affine triple progression.
theorem transitionStackRouteSubtractCount_rows
(amount : Nat) (progression : AffineUnaryTripleProgression) :
affineUnaryTripleProgressionRows
(transitionStackRouteSubtractCount amount progression) =
(affineUnaryTripleProgressionRows progression).take
(progression.count - amount) := by
rw [affineUnaryTripleProgressionRows_eq_ofFn,
affineUnaryTripleProgressionRows_eq_ofFn]
have hcount : progression.count - amount ≤ progression.count :=
Nat.sub_le progression.count amount
rw [← Fin.ofFn_take_eq_take_ofFn hcount]
apply List.ofFn_inj.mpr
funext index
simp [transitionStackRouteSubtractCount, Fin.take]end CLRS.Chapter34.Turing.CookLevin