Round evaluation at the unchanged first-phase parameters

The explicit first-phase chooser also satisfies both short-call guards and the growing final-call guard of an affine round. Canonical evaluation therefore needs no additional numerical premise. This concerns source widths and execution only: it supplies no entropy, independence, or error guarantee for the round's current row or either original source.

theorem Algebraic.Cutwidth.Extractor.affineRoundParameters_right_guard (n t a target : ℕ) : MatchedBlockRuntimeValid (affinePhaseOneRightBits n t a target) 24 (affinePhaseOneScale n t a target) (affinePhaseOneLocalError target)

The chosen original right-source width fits both depth-twenty-four calls.

theorem Algebraic.Cutwidth.Extractor.affineRoundParameters_row_guard (n t a target : ℕ) : MatchedBlockRuntimeValid (matchedBlockOutputBits (growingMatchedBlockDepth t) (affinePhaseOneScale n t a target)) 24 (affinePhaseOneScale n t a target) (affinePhaseOneLocalError target)

The entire chosen long row fits the middle depth-twenty-four call.

theorem Algebraic.Cutwidth.Extractor.affineRoundParameters_runtime_eq (n t a target : ℕ) (x : Fin n → Bool) (y : Fin (affinePhaseOneRightBits n t a target) → Bool) (row : Fin (matchedBlockOutputBits (growingMatchedBlockDepth t) (affinePhaseOneScale n t a target)) → Bool) : affineRoundRuntime t (affinePhaseOneScale n t a target) (affinePhaseOneLocalError target) (List.ofFn x) (List.ofFn y) (List.ofFn row) = List.ofFn (affineRoundOutput n (affinePhaseOneRightBits n t a target) (growingMatchedBlockDepth t) (affinePhaseOneScale n t a target) (affinePhaseOneLocalError target) x y row)

The actual round evaluator agrees with the semantic program at every chosen parameter tuple.