MachineBinaryInputReduction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The complete ordinary-binary input bridge. Arbitrary raw input bits are first validated and retained, or replaced by a fixed contradictory encoded formula. The checked occurrence-index renamer then emits the inherited dense 3CNF codec. Both stages and their physical handoff have actual polynomial-time finite-alphabet machine certificates.

This is a bridge for the explicit ordinary binary 3SAT language. It is not the PCP construction, a proof of that construction's runtime, or an NP-hardness assertion about the eventual 2-to-1 target.

def OAI.MaxCutGames.BinaryInputReduction.computation line 26
Source documentation
The actual sequential machine handles every bitstring, including malformed and noncanonical encodings, and outputs the fixed dense formula serialization.
```
noncomputable def computation :
    TM2ComputableInPolyTime (id : List Bool → List Bool) formulaBits BinaryLanguage.totalRename := by
…
```
Mentions: OAI.MaxCutGames.BinaryLanguage.totalRename
theorem OAI.MaxCutGames.BinaryInputReduction.computation_finiteAlphabet line 33
def OAI.MaxCutGames.BinaryInputReduction.reduction line 41
Source documentation
Satisfiability equivalence plus an actual raw-bit machine; no external verifier, parsing-time assertion, or recoding hypothesis is an input.
```
noncomputable def reduction : CookLevin.PolynomialThreeSATReduction BinaryLanguage.language where
…
```
Mentions: OAI.MaxCutGames.BinaryLanguage.language
theorem OAI.MaxCutGames.BinaryInputReduction.reduction_finiteAlphabet line 46