MachineBinaryFormulaLemmas.lean`

79 declarations, 0 contain sorry, 0 declared as axioms

An explicit ordinary-binary codec for sparse-name three-literal CNF.

A natural name uses its canonical little-endian binary digits. Each payload digit b is represented by the pair true,b; false terminates the name. Zero has the empty payload and therefore the one-bit encoding [false]. A literal is its sign bit followed by its name. A clause contains three literal encodings. A formula contains true followed by each clause, then one final false. There is no unary expansion of a variable name, declared variable universe, or deduplication of literal or clause occurrences.

The parser rejects noncanonical name payloads, incomplete literals/clauses, and trailing input. The input length is within a fixed factor of the total ordinary binary name lengths plus signs and clause framing. Machine correspondence and runtime are proved separately; these output-size bounds are not time bounds.

def OAI.UniqueGamesTheorem.BinaryFormula.clauseNames line 18
Source documentation
An ordinary conjunction of three-slot clauses with sparse variable names. Repeated names and repeated literals are permitted in every clause.
```
def clauseNames (c : Clause) : List Nat :=
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryFormula.Clause
def OAI.UniqueGamesTheorem.BinaryFormula.sourceNames line 21
def OAI.UniqueGamesTheorem.BinaryFormula.activeNames line 26
Source documentation
Explicit list of occurring names, with duplicates removed. The list lengths depend only on occurrences; no interval of natural-number names is enumerated.
```
def activeNames (F : Formula) : List Nat :=
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryFormula.Formula
theorem OAI.UniqueGamesTheorem.BinaryFormula.literal_mem_active line 29
def OAI.UniqueGamesTheorem.BinaryFormula.compactIndex line 37
def OAI.UniqueGamesTheorem.BinaryFormula.decodeName line 41
def OAI.UniqueGamesTheorem.BinaryFormula.compactLiteral line 44
def OAI.UniqueGamesTheorem.BinaryFormula.compactClause line 48
def OAI.UniqueGamesTheorem.BinaryFormula.compactClauses line 54
def OAI.UniqueGamesTheorem.BinaryFormula.dense line 57
def OAI.UniqueGamesTheorem.BinaryFormula.restrictAssignment line 61
def OAI.UniqueGamesTheorem.BinaryFormula.extendAssignment line 64
theorem OAI.UniqueGamesTheorem.BinaryFormula.decode_compactIndex line 68
theorem OAI.UniqueGamesTheorem.BinaryFormula.compactIndex_injective line 74
Source documentation
Distinct occurring names remain distinct. Repeated occurrences of one name use the same index, since the proof argument of compactIndex is irrelevant.
```
theorem compactIndex_injective (F : Formula) (u v : Nat)
    (hu : u ∈ activeNames F) (hv : v ∈ activeNames F)
    (h : compactIndex F u hu = compactIndex F v hv) : u = v := by
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryFormula.Formula, OAI.UniqueGamesTheorem.BinaryFormula.activeNames, OAI.UniqueGamesTheorem.BinaryFormula.compactIndex
theorem OAI.UniqueGamesTheorem.BinaryFormula.compactLiteral_positive line 80
theorem OAI.UniqueGamesTheorem.BinaryFormula.eval_compact_restrict line 83
theorem OAI.UniqueGamesTheorem.BinaryFormula.eval_compact_extend line 89
def OAI.UniqueGamesTheorem.BinaryFormula.evaluationList line 99
theorem OAI.UniqueGamesTheorem.BinaryFormula.evaluationList_restrict line 104
Source documentation
Evaluation lists retain every clause occurrence, so this is stronger than merely preserving satisfiability or the set of distinct clauses.
```
theorem evaluationList_restrict (F : Formula) (A : Nat → Bool) :
    PCP.NameCompaction.evaluationList (dense F) (restrictAssignment F A) =
      evaluationList F A := by
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryFormula.Formula, OAI.UniqueGamesTheorem.BinaryFormula.dense, OAI.UniqueGamesTheorem.BinaryFormula.restrictAssignment, OAI.UniqueGamesTheorem.BinaryFormula.evaluationList
theorem OAI.UniqueGamesTheorem.BinaryFormula.evaluationList_extend line 112
def OAI.UniqueGamesTheorem.BinaryFormula.failedCount line 126
theorem OAI.UniqueGamesTheorem.BinaryFormula.failedCount_restrict line 129
theorem OAI.UniqueGamesTheorem.BinaryFormula.failedCount_extend line 133
theorem OAI.UniqueGamesTheorem.BinaryFormula.clauseNames_flat_length line 137
theorem OAI.UniqueGamesTheorem.BinaryFormula.dense_clause_count line 146
theorem OAI.UniqueGamesTheorem.BinaryFormula.dense_variable_bound line 152
Source documentation
No greatest-name bound occurs: even very large, sparsely used names yield at most three dense variables per explicitly listed clause.
```
theorem dense_variable_bound (F : Formula) :
    (dense F).variables ≤ 3 * F.clauses.length := by
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryFormula.Formula, OAI.UniqueGamesTheorem.BinaryFormula.dense
theorem OAI.UniqueGamesTheorem.BinaryFormula.dense_completeness line 157
theorem OAI.UniqueGamesTheorem.BinaryFormula.dense_reflects line 166
theorem OAI.UniqueGamesTheorem.BinaryFormula.dense_satisfiable_iff line 176
theorem OAI.UniqueGamesTheorem.BinaryFormula.dense_preserves_gap line 180
theorem OAI.UniqueGamesTheorem.BinaryFormula.dense_encoding_bound line 190
Source documentation
Size of the reused dense formula encoding, bounded only by the number of explicit clause occurrences. This does not assert a binary input parser or a running-time bound for sparse-to-dense conversion.
```
theorem dense_encoding_bound (F : Formula) :
    (Complexity.formulaBits (dense F)).length ≤
      9 * F.clauses.length * F.clauses.length + 10 * F.clauses.length + 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryFormula.Formula, OAI.UniqueGamesTheorem.BinaryFormula.dense
theorem OAI.UniqueGamesTheorem.BinaryEncoding.bitsValue_bits line 234
def OAI.UniqueGamesTheorem.BinaryEncoding.frame line 242
Source documentation
Prefix-free framing on the two-symbol input alphabet.
```
def frame : List Bool → List Bool
  | [] => [false]
  | b :: bits => true :: b :: frame bits
```
theorem OAI.UniqueGamesTheorem.BinaryEncoding.parseFrame_encoded line 246
theorem OAI.UniqueGamesTheorem.BinaryEncoding.frame_length line 252
def OAI.UniqueGamesTheorem.BinaryEncoding.nameBits line 258
theorem OAI.UniqueGamesTheorem.BinaryEncoding.parseName_encoded line 262
Source documentation
Equality with the canonical digits rejects alternate padded encodings.
```
@[simp] theorem parseName_encoded (name : Nat) (rest : List Bool) :
    parseName (nameBits name ++ rest) = some (name, rest) := by
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryEncoding.parseName, OAI.UniqueGamesTheorem.BinaryEncoding.nameBits
theorem OAI.UniqueGamesTheorem.BinaryEncoding.nameBits_length line 266
theorem OAI.UniqueGamesTheorem.BinaryEncoding.nameBits_length_le_of_lt_pow line 270
def OAI.UniqueGamesTheorem.BinaryEncoding.literalBits line 276
theorem OAI.UniqueGamesTheorem.BinaryEncoding.parseLiteral_encoded line 279
theorem OAI.UniqueGamesTheorem.BinaryEncoding.literalBits_length line 284
def OAI.UniqueGamesTheorem.BinaryEncoding.clauseBits line 288
theorem OAI.UniqueGamesTheorem.BinaryEncoding.clause_three_entries line 291
theorem OAI.UniqueGamesTheorem.BinaryEncoding.parseClause_encoded line 297
def OAI.UniqueGamesTheorem.BinaryEncoding.clauseNameSize line 301
theorem OAI.UniqueGamesTheorem.BinaryEncoding.clauseBits_length line 304
def OAI.UniqueGamesTheorem.BinaryEncoding.clausesBits line 309
def OAI.UniqueGamesTheorem.BinaryEncoding.formulaBits line 313
def OAI.UniqueGamesTheorem.BinaryEncoding.namesBitSize line 315
theorem OAI.UniqueGamesTheorem.BinaryEncoding.namesBitSize_nil line 318
theorem OAI.UniqueGamesTheorem.BinaryEncoding.namesBitSize_cons line 320
theorem OAI.UniqueGamesTheorem.BinaryEncoding.clausesBits_length line 324
theorem OAI.UniqueGamesTheorem.BinaryEncoding.formulaBits_length line 333
theorem OAI.UniqueGamesTheorem.BinaryEncoding.clauses_length_lt_bits line 338
def OAI.UniqueGamesTheorem.BinaryEncoding.ordinarySize line 345
Source documentation
Binary digits, one sign per literal, and one terminal bit form a natural reference size. The concrete framing adds only a fixed multiplicative factor.
```
def ordinarySize (formula : Formula) : Nat :=
…
```
theorem OAI.UniqueGamesTheorem.BinaryEncoding.ordinarySize_le_bits line 348
theorem OAI.UniqueGamesTheorem.BinaryEncoding.bits_le_three_ordinarySize line 354
theorem OAI.UniqueGamesTheorem.BinaryEncoding.parseClauses_encoded line 362
Source documentation
Fuel bounds the number of clause iterations, not the size of any name.
```
@[simp] theorem parseClauses_encoded (clauses : List Clause) (rest : List Bool)
    (fuel : Nat) (enough : clauses.length < fuel) :
    parseClauses fuel (clausesBits clauses ++ rest) = some (clauses, rest) := by
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryEncoding.parseClauses, OAI.UniqueGamesTheorem.BinaryEncoding.clausesBits
theorem OAI.UniqueGamesTheorem.BinaryEncoding.decodeFormula_encoded line 377
theorem OAI.UniqueGamesTheorem.BinaryEncoding.formulaBits_injective line 387
Source documentation
This preserves every literal and clause occurrence, including duplicates.
```
theorem formulaBits_injective {first second : Formula}
    (same : formulaBits first = formulaBits second) : first = second := by
…
```
Mentions: OAI.UniqueGamesTheorem.BinaryEncoding.formulaBits
theorem OAI.UniqueGamesTheorem.BinaryEncoding.dense_encoding_bound line 394
Source documentation
The existing dense unary output is polynomial in this ordinary binary input length. This remains an output-size theorem, not a runtime certificate.
```
theorem dense_encoding_bound (formula : Formula) :
    (UniqueGamesTheorem.Foundations.Complexity.formulaBits (dense formula)).length ≤
      9 * (formulaBits formula).length * (formulaBits formula).length +
      10 * (formulaBits formula).length + 2 := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.formulaBits, OAI.UniqueGamesTheorem.BinaryEncoding.formulaBits
theorem OAI.UniqueGamesTheorem.BinaryOccurrenceRename.literal_mem_names line 426
def OAI.UniqueGamesTheorem.BinaryOccurrenceRename.nameIndex line 433
def OAI.UniqueGamesTheorem.BinaryOccurrenceRename.literal line 437
def OAI.UniqueGamesTheorem.BinaryOccurrenceRename.clause line 441
def OAI.UniqueGamesTheorem.BinaryOccurrenceRename.renamed line 447
def OAI.UniqueGamesTheorem.BinaryOccurrenceRename.restrictAssignment line 451
def OAI.UniqueGamesTheorem.BinaryOccurrenceRename.extendAssignment line 455
theorem OAI.UniqueGamesTheorem.BinaryOccurrenceRename.nameIndex_reads_name line 458
theorem OAI.UniqueGamesTheorem.BinaryOccurrenceRename.clause_eval_restrict line 462
theorem OAI.UniqueGamesTheorem.BinaryOccurrenceRename.clause_eval_extend line 467
theorem OAI.UniqueGamesTheorem.BinaryOccurrenceRename.renamed_clause_count line 477
theorem OAI.UniqueGamesTheorem.BinaryOccurrenceRename.renamed_variable_count line 480
theorem OAI.UniqueGamesTheorem.BinaryOccurrenceRename.renamed_satisfiable_iff line 484
theorem OAI.UniqueGamesTheorem.BinaryOccurrenceRename.nat_bits_injective line 499
theorem OAI.UniqueGamesTheorem.BinaryOccurrenceRename.idxOf_binary_payloads line 506
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.UniqueGamesTheorem.BinaryOccurrenceRename.renamed_encoding_bound line 519
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.UniqueGamesTheorem.BinaryOccurrenceRename.renamed
theorem OAI.UniqueGamesTheorem.BinaryOccurrenceRename.renamed_encoding_bound_bits line 526