MachineBinaryInputReductionLemmas.lean`

29 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.UniqueGamesTheorem.BinaryInputReduction.computation line 30
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.UniqueGamesTheorem.BinaryLanguage.totalRename
theorem OAI.UniqueGamesTheorem.BinaryInputReduction.computation_finiteAlphabet line 37
def OAI.UniqueGamesTheorem.BinaryInputReduction.reduction line 45
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.UniqueGamesTheorem.BinaryLanguage.language
theorem OAI.UniqueGamesTheorem.BinaryInputReduction.reduction_finiteAlphabet line 50
def OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.permutationEquiv line 66
Source documentation
The full forward and inverse tables already prove the permutation laws.
```
def permutationEquiv {q : Nat} (table : PermutationTable q) : Equiv.Perm (Fin q) where
…
```
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.no_loops line 77
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.no_reverse line 85

theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.undirected_unique line 95

Source documentation

Simplicity concerns unordered endpoint pairs, independently of how an edge could have been presented before the canonical bipartite orientation.

theorem undirected_unique (i j : Fin game.constraints.length)
    (same :
      (game.constraints[i].source = game.constraints[j].source ∧
        game.constraints[i].target = game.constraints[j].target) ∨
      (game.constraints[i].source = game.constraints[j].target ∧
        game.constraints[i].target = game.constraints[j].source)) : i = j := by
…

def OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame line 107
Source documentation
The list presentation yields exactly the bipartite occurrence abstraction used by the subdivision proof, without quotienting or discarding occurrences.
```
def toBipartiteGame : BipartiteGame
    {v : Fin game.vertices // presentation.side v = false}
    {v : Fin game.vertices // presentation.side v = true}
    (Fin game.constraints.length) (Fin q) where
…
```
Mentions: OAI.UniqueGamesTheorem.Explicit.BipartiteGame

theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_satisfied_iff line 123

Source documentation

Restricting one vertex labeling to the two sides preserves every individual constraint's satisfaction predicate, hence its original occurrence identity.

theorem toBipartiteGame_satisfied_iff (labeling : Fin game.vertices → Fin q)
    (i : Fin game.constraints.length) :
    presentation.toBipartiteGame.Satisfied
      (fun v => labeling v.val) (fun v => labeling v.val) i ↔
      game.constraints[i].satisfied labeling = true := by
…

def OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.mergeLabelings line 133
Source documentation
Two independently chosen side labelings give one total labeling because every vertex has exactly one Boolean side. Isolated vertices cause no exception.
```
def mergeLabelings
    (left : {v : Fin game.vertices // presentation.side v = false} → Fin q)
    (right : {v : Fin game.vertices // presentation.side v = true} → Fin q) :
    Fin game.vertices → Fin q := fun v =>
…
```
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.mergeLabelings_left line 140
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.mergeLabelings_right line 147
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_count line 154
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_count_merge line 168
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_maxSatisfied line 176
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_value line 194
Source documentation
The abstract bipartite game and the actual serialized list instance have exactly the same value, including the same denominator of edge occurrences.
```
theorem toBipartiteGame_value :
    presentation.toBipartiteGame.value = Integration.InstanceValue.value game := by
…
```
Mentions: OAI.UniqueGamesTheorem.Integration.InstanceValue.value
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction.nonempty line 210
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction.occurrence_count_positive line 213
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction.completeness_value line 217
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction.soundness_value line 224
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction.alphabet_eq_two_pow line 233
Source documentation
The fixed coordinate equivalence forces the explicit table alphabet to have exactly the requested binary-vector cardinality.
```
theorem alphabet_eq_two_pow : reduction.alphabet = 2 ^ reduction.dimension := by
…
```
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction.no_loops line 237
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction.undirected_unique line 243
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction.full_table_length line 258
Source documentation
Every occurrence serializes all forward-table entries, not an oracle or an intensional description of the constraint.
```
theorem full_table_length (input : List Bool)
    (i : Fin (reduction.construct input).constraints.length) :
    (Complexity.tableWords
      (reduction.construct input).constraints[i].permutation).length = reduction.alphabet :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction.translation_equation line 264
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction.decode_output line 275
Source documentation
The machine's exact output bits decode to the same ordered occurrence list, with the same endpoints and all the same permutation tables.
```
theorem decode_output (input : List Bool) :
    Complexity.decodeGameBits reduction.alphabet
      (Complexity.gameBits (reduction.construct input)) =
        some (reduction.construct input) :=
…
```
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction.output_word_count line 281
theorem OAI.UniqueGamesTheorem.Explicit.MachineOutputContract.BinaryGapReduction.malformed_soundness line 288
Source documentation
Malformed words are in the NO language and are processed by the same fixed machine; they do not need an extra promised-input condition.
```
theorem malformed_soundness (input : List Bool)
    (malformed : BinaryEncoding.decodeFormula input = none) :
    ∀ labeling, (countSatisfied labeling (reduction.construct input).constraints : ℝ) /
      (reduction.construct input).constraints.length ≤ δ := by
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryEncoding.decodeFormula