MachineBinaryParsing.lean`

69 declarations, 0 contain sorry, 0 declared as axioms

Soundness of the ordinary-binary parser and its concrete name-scanning machine. Every successful parse consumes exactly a canonical encoding and leaves its stated suffix. Thus malformed or noncanonical bitstrings cannot name an extra formula. The finite scanner's final-digit test is proved equivalent to the codec's arithmetic canonicality test.

theorem OAI.MaxCutGames.BinaryParsing.frame_eq line 21
theorem OAI.MaxCutGames.BinaryParsing.canonical_cons_cons line 26
theorem OAI.MaxCutGames.BinaryParsing.canonical_iff line 31
Source documentation
A payload has no redundant high zero precisely when its last digit is one, with the empty payload representing zero.
```
theorem canonical_iff (bits : List Bool) :
    BinaryNameMachine.canonical bits = true ↔ (bitsValue bits).bits = bits := by
…
```
Mentions: OAI.MaxCutGames.BinaryNameMachine.canonical
theorem OAI.MaxCutGames.BinaryParsing.canonical_nat_bits line 56
theorem OAI.MaxCutGames.BinaryParsing.parseFrame_sound line 61
theorem OAI.MaxCutGames.BinaryParsing.parseName_sound line 85
theorem OAI.MaxCutGames.BinaryParsing.parseLiteral_sound line 101
theorem OAI.MaxCutGames.BinaryParsing.parseClause_sound line 116
theorem OAI.MaxCutGames.BinaryParsing.parseClauses_sound line 140
theorem OAI.MaxCutGames.BinaryParsing.decodeFormula_sound line 168
theorem OAI.MaxCutGames.BinaryParsing.decodeFormula_eq_some_iff line 182
theorem OAI.MaxCutGames.BinaryParsing.scanSpec_nameBits line 188
Source documentation
Exact agreement of the finite-state name scanner with a canonical encoded name, including the untouched suffix and the actual binary payload stack.
```
theorem scanSpec_nameBits (name : Nat) (suffix output : List Bool) :
    BinaryNameMachine.scanSpec (nameBits name ++ suffix) output none =
      ⟨true, suffix, name.bits.reverse ++ output⟩ := by
…
```
Mentions: OAI.MaxCutGames.BinaryNameMachine.scanSpec
theorem OAI.MaxCutGames.BinaryOccurrenceRename.literal_mem_names line 216
def OAI.MaxCutGames.BinaryOccurrenceRename.nameIndex line 223
def OAI.MaxCutGames.BinaryOccurrenceRename.literal line 227
def OAI.MaxCutGames.BinaryOccurrenceRename.clause line 231
def OAI.MaxCutGames.BinaryOccurrenceRename.renamed line 237
def OAI.MaxCutGames.BinaryOccurrenceRename.restrictAssignment line 241
def OAI.MaxCutGames.BinaryOccurrenceRename.extendAssignment line 245
theorem OAI.MaxCutGames.BinaryOccurrenceRename.nameIndex_reads_name line 248
theorem OAI.MaxCutGames.BinaryOccurrenceRename.clause_eval_restrict line 252
theorem OAI.MaxCutGames.BinaryOccurrenceRename.clause_eval_extend line 257
theorem OAI.MaxCutGames.BinaryOccurrenceRename.renamed_clause_count line 267
theorem OAI.MaxCutGames.BinaryOccurrenceRename.renamed_variable_count line 270
theorem OAI.MaxCutGames.BinaryOccurrenceRename.renamed_satisfiable_iff line 274
theorem OAI.MaxCutGames.BinaryOccurrenceRename.nat_bits_injective line 289
theorem OAI.MaxCutGames.BinaryOccurrenceRename.idxOf_binary_payloads line 296
Source documentation
The numerical first occurrence is exactly the index found by comparing binary payload lists. This is the key search-machine correspondence.
```
theorem idxOf_binary_payloads (names : List Nat) (name : Nat) :
    (names.map Nat.bits).idxOf name.bits = names.idxOf name := by
…
```
theorem OAI.MaxCutGames.BinaryOccurrenceRename.renamed_encoding_bound line 309
Source documentation
The fixed unary output codec has quadratic size in the literal count.
```
theorem renamed_encoding_bound (F : Formula) :
    (Complexity.formulaBits (renamed F)).length ≤
      9 * F.clauses.length * F.clauses.length + 10 * F.clauses.length + 2 := by
…
```
Mentions: OAI.MaxCutGames.BinaryOccurrenceRename.renamed
theorem OAI.MaxCutGames.BinaryOccurrenceRename.renamed_encoding_bound_bits line 316
def OAI.MaxCutGames.BinaryLanguage.rejectBinary line 339
theorem OAI.MaxCutGames.BinaryLanguage.rejectBinary_unsatisfiable line 343
def OAI.MaxCutGames.BinaryLanguage.rejectFormula line 352
theorem OAI.MaxCutGames.BinaryLanguage.reject_unsatisfiable line 354
def OAI.MaxCutGames.BinaryLanguage.language line 358
def OAI.MaxCutGames.BinaryLanguage.totalParsed line 361
def OAI.MaxCutGames.BinaryLanguage.totalRename line 364
theorem OAI.MaxCutGames.BinaryLanguage.totalParsed_satisfiable_iff line 367
theorem OAI.MaxCutGames.BinaryLanguage.totalRename_satisfiable_iff line 373
theorem OAI.MaxCutGames.BinaryLanguage.totalRename_encoded line 378
theorem OAI.MaxCutGames.BinaryLanguage.language_encoded line 382
theorem OAI.MaxCutGames.BinaryLanguage.reject_bits_length line 386
theorem OAI.MaxCutGames.BinaryLanguage.totalRename_output_length line 388
structure OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite line 414
Source documentation
A canonical orientation from the false side to the true side. Injectivity is on occurrence indices, so two distinct list entries cannot be parallel even when their constraint tables are different.
```
structure SimpleBipartite {q : Nat} (game : Instance q) where
…
```
def OAI.MaxCutGames.Explicit.MachineOutputContract.permutationEquiv line 424
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.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.no_loops line 435
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.no_reverse line 443

theorem OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.undirected_unique line 453

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.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame line 465
Source documentation
The list presentation yields exactly the bipartite occurrence abstraction used by the v2 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.MaxCutGames.Explicit.BipartiteGame

theorem OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_satisfied_iff line 481

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.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.mergeLabelings line 491
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.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.mergeLabelings_left line 498
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.mergeLabelings_right line 505
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_count line 512
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_count_merge line 526
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_maxSatisfied line 534
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.SimpleBipartite.toBipartiteGame_value line 552
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.MaxCutGames.Integration.InstanceValue.value
structure OAI.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction line 563
Source documentation
Every parameter, coordinate identification, program, and polynomial is fixed before the input quantifier. The identity input encoding measures runtime in the original raw bit length, including sparse binary variable names.
```
structure BinaryGapReduction (ε δ : ℝ) where
…
```
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction.nonempty line 588
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction.occurrence_count_positive line 591
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction.completeness_value line 595
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction.soundness_value line 602
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction.alphabet_eq_two_pow line 611
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.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction.no_loops line 615
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction.undirected_unique line 621
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction.full_table_length line 636
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.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction.translation_equation line 642
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction.decode_output line 653
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.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction.output_word_count line 659
theorem OAI.MaxCutGames.Explicit.MachineOutputContract.BinaryGapReduction.malformed_soundness line 666
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.MaxCutGames.BinaryEncoding.decodeFormula