CLRS-Lean
Chapter 34. NP-Completeness
34.4. NP-Completeness Proofs
34.4. Verified bounded TM2 builders
34.4. Affine progression sources for complete mux invocations

Imports

import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.AffineUnaryTripleProgressionFixedGroups
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.MuxFin

Affine progression sources for complete mux invocations

A whole-row mux coordinate needs three unary triples. The arithmetic content of those triples can be compressed to one ordinary triple progression: (whenTrue, whenFalse, trueArm). A singleton header progression carries the shared selector, its negation wire, and a flag saying whether this segment starts a new mux invocation. Existing fixed-group progression machinery can therefore generate a compact, segment-delimited source without adding a new arithmetic oracle.

The subsequent streaming controller only has to retain the two selector fields and expand each data triple to the exact AffineMuxFinPairFrame protocol.

noncomputable sectionnamespace CLRS.Chapter34.Turing.PolyBuilder

One affine segment of a canonical mux invocation. trueArmBase denotes the first fresh true-arm AND output; the corresponding false-arm output is always the following wire.

structure AffineMuxInvocationProgression where
  selector : Nat
  selectorNot : Nat
  emitsHeader : Bool
  whenTrueBase : Nat
  whenFalseBase : Nat
  trueArmBase : Nat
  whenTrueStep : Nat
  whenFalseStep : Nat
  trueArmStep : Nat
  count : Nat
deriving DecidableEq, Repr

Singleton metadata progression. Its third field is the unary Boolean header flag.

def AffineMuxInvocationProgression.headerProgression
    (segment : AffineMuxInvocationProgression) :
    AffineUnaryTripleProgression :=
  { base₁ := segment.selector
    base₂ := segment.selectorNot
    base₃ := if segment.emitsHeader then 1 else 0
    step₁ := 0
    step₂ := 0
    step₃ := 0
    count := 1 }

The three genuinely varying values of each mux coordinate.

def AffineMuxInvocationProgression.dataProgression
    (segment : AffineMuxInvocationProgression) :
    AffineUnaryTripleProgression :=
  { base₁ := segment.whenTrueBase
    base₂ := segment.whenFalseBase
    base₃ := segment.trueArmBase
    step₁ := segment.whenTrueStep
    step₂ := segment.whenFalseStep
    step₃ := segment.trueArmStep
    count := segment.count }

The fixed two-progression source block of one invocation segment.

def AffineMuxInvocationProgression.sourceProgressions
    (segment : AffineMuxInvocationProgression) :
    List AffineUnaryTripleProgression :=
  [segment.headerProgression, segment.dataProgression]

Runtime descriptor encoding accepted by the existing triple-progression family controller.

def encodeAffineMuxInvocationProgressionFamily
    (segments : List AffineMuxInvocationProgression) :
    List UnaryFrameSym :=
  encodeAffineUnaryTripleProgressionFamily
    (segments.flatMap AffineMuxInvocationProgression.sourceProgressions)

Concrete data triples generated by one segment.

def AffineMuxInvocationProgression.dataRows
    (segment : AffineMuxInvocationProgression) :
    List (Nat × Nat × Nat) :=
  affineUnaryTripleProgressionRows segment.dataProgression

Reconstruct one canonical mux frame from a generated data triple.

def AffineMuxInvocationProgression.frameOfRow
    (segment : AffineMuxInvocationProgression)
    (row : Nat × Nat × Nat) : AffineMuxFinPairFrame :=
  { whenTrue := row.1
    whenFalse := row.2.1
    selector := segment.selector
    selectorNot := segment.selectorNot
    trueArm := row.2.2
    falseArm := row.2.2 + 1 }

Exact mux frames denoted by one affine segment.

def AffineMuxInvocationProgression.frames
    (segment : AffineMuxInvocationProgression) :
    List AffineMuxFinPairFrame :=
  segment.dataRows.map segment.frameOfRow

Optional canonical mux header. Only the first segment of a mux emits it.

def AffineMuxInvocationProgression.headerFrames
    (segment : AffineMuxInvocationProgression) : List UnaryFrameSym :=
  if segment.emitsHeader then encodeAffineMuxFinHeader segment.selector else []

Exact final mux-controller bytes contributed by one segment.

def AffineMuxInvocationProgression.invocationFrames
    (segment : AffineMuxInvocationProgression) : List UnaryFrameSym :=
  segment.headerFrames ++
    segment.frames.flatMap encodeAffineMuxFinPairFrame

Delimiter-bearing output of the existing arithmetic source before mux protocol expansion.

def AffineMuxInvocationProgression.sourceFrames
    (segment : AffineMuxInvocationProgression) : List UnaryFrameSym :=
  affineUnaryTripleProgressionFrameStream segment.headerProgression ++
    affineUnaryTripleProgressionFrameStream segment.dataProgression ++
    [.frameEnd]

Complete fixed-group arithmetic source for a segment family.

def affineMuxInvocationProgressionFamilySourceFrames
    (segments : List AffineMuxInvocationProgression) :
    List UnaryFrameSym :=
  affineUnaryTripleProgressionFixedGroupFrameStream 1
    (segments.flatMap AffineMuxInvocationProgression.sourceProgressions)

@[simp] theorem
    AffineMuxInvocationProgression.headerProgression_frameStream
    (segment : AffineMuxInvocationProgression) :
    affineUnaryTripleProgressionFrameStream segment.headerProgression =
      encodeUnaryFrame
        [segment.selector, segment.selectorNot,
          if segment.emitsHeader then 1 else 0] := by
  simp [AffineMuxInvocationProgression.headerProgression,
    affineUnaryTripleProgressionFrameStream,
    affineUnaryTripleProgressionRows,
    affineUnaryTripleProgressionRowsFrom, affineUnaryTripleRowValues]

The fixed group marker occurs exactly after each header/data pair.

theorem affineMuxInvocationProgressionFamilySourceFrames_eq
    (segments : List AffineMuxInvocationProgression) :
    affineMuxInvocationProgressionFamilySourceFrames segments =
      segments.flatMap AffineMuxInvocationProgression.sourceFrames := by
  unfold affineMuxInvocationProgressionFamilySourceFrames
  induction segments with
  | nil => rfl
  | cons segment segments ih =>
      simp [AffineMuxInvocationProgression.sourceProgressions,
        AffineMuxInvocationProgression.sourceFrames,
        affineUnaryTripleProgressionFixedGroupFrameStream,
        affineUnaryTripleProgressionFixedGroupFrameStreamFrom,
        List.append_assoc]
      simpa [affineUnaryTripleProgressionFixedGroupFrameStream] using ih

Positional closed form of the segment frames.


theorem AffineMuxInvocationProgression.frames_eq_ofFn
    (segment : AffineMuxInvocationProgression) :
    segment.frames =
      List.ofFn fun coordinate : Fin segment.count =>
        { whenTrue := segment.whenTrueBase +
            coordinate.val * segment.whenTrueStep
          whenFalse := segment.whenFalseBase +
            coordinate.val * segment.whenFalseStep
          selector := segment.selector
          selectorNot := segment.selectorNot
          trueArm := segment.trueArmBase +
            coordinate.val * segment.trueArmStep
          falseArm := segment.trueArmBase +
            coordinate.val * segment.trueArmStep + 1 } := by
  unfold AffineMuxInvocationProgression.frames
    AffineMuxInvocationProgression.dataRows
  rw [affineUnaryTripleProgressionRows_eq_ofFn, List.map_ofFn]
  apply List.ofFn_inj.mpr
  funext coordinate
  rfl



@[simp] theorem AffineMuxInvocationProgression.frames_length
    (segment : AffineMuxInvocationProgression) :
    segment.frames.length = segment.count := by
  rw [segment.frames_eq_ofFn]
  simp

end CLRS.Chapter34.Turing.PolyBuilder