TableKeysAddressGame.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

Direct addresses for the v2 single-orbit matrix game. There is one canonical body address space, with no side bit and no extra right-endpoint offset. Unused addresses are isolated. Runtime construction uses canonical words and radix arithmetic, not deduplication or inverse vertex enumeration.

abbrev OAI.MaxCutGames.Decoder.TableKeysAddressGame.vertexCount line 20
def OAI.MaxCutGames.Decoder.TableKeysAddressGame.vertexAddress line 23
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.vertexAddress_injective line 26
def OAI.MaxCutGames.Decoder.TableKeysAddressGame.queryAddress line 33
Source documentation
Both endpoints use this same routine and this same address block.
```
def queryAddress (S : Source) (k s d : Nat) (q : TableKeysGame.Query S k s d) :
    Fin (vertexCount S k s d) :=
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.Query, OAI.MaxCutGames.Decoder.TableKeysAddressGame.vertexCount
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.vertexAddress_query line 37
def OAI.MaxCutGames.Decoder.TableKeysAddressGame.explicitToAddress line 43
Source documentation
This inverse is a proof adapter only; the output constructor never calls it.
```
def explicitToAddress (S : Source) (k s d : Nat) :
    Fin (TableKeysGame.explicitVertexCount S k s d) → Fin (vertexCount S k s d) :=
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.explicitVertexCount, OAI.MaxCutGames.Decoder.TableKeysAddressGame.vertexCount
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.explicitToAddress_injective line 47
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.explicitToAddress_apply line 52
def OAI.MaxCutGames.Decoder.TableKeysAddressGame.semanticToAddress line 58
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.semanticToAddress_injective line 62
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.semanticToAddress_apply line 67
def OAI.MaxCutGames.Decoder.TableKeysAddressGame.addressEdge line 73
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.addressEdge_eq_embed line 81
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.addressEdge_eq_semantic_embed line 88
def OAI.MaxCutGames.Decoder.TableKeysAddressGame.outputInstance line 96
Source documentation
The correcting function is not evaluated when producing an edge list.
```
def outputInstance (S : Source) (k : Nat) {s d : Nat} (g : SplitGadget s d)
    (en : NoiseEnumeration g) : Instance (2^s) where
…
```
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.outputInstance_eq_embed line 108
Source documentation
Every occurrence, its order, and its full permutation table are retained.
```
theorem outputInstance_eq_embed (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (en : NoiseEnumeration g) :
    outputInstance S k g en =
      embedInstance (TableKeysGame.outputInstanceWithEnumeration S k g en)
        (explicitToAddress S k s d) (explicitToAddress_injective S k s d) := by
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysAddressGame.outputInstance, OAI.MaxCutGames.Decoder.TableKeysGame.outputInstanceWithEnumeration, OAI.MaxCutGames.Decoder.TableKeysAddressGame.explicitToAddress, OAI.MaxCutGames.Decoder.TableKeysAddressGame.explicitToAddress_injective
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.outputInstance_length line 117
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.outputInstance_count line 124
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.completeAt_outputInstance_iff_explicit line 135
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.soundAt_outputInstance_iff_explicit line 142
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.completeAt_outputInstance_iff line 149
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.soundAt_outputInstance_iff line 156
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.outputInstance_translations line 163
def OAI.MaxCutGames.Decoder.TableKeysAddressGame.tableOutput line 181
Source documentation
Fixed finite noise data suffice for executable output.
```
def tableOutput (S : Source) (k : Nat) {s d : Nat} (T : Integration.NoiseTables.Table s d) :
    Instance (2^s) :=
…
```
Mentions: OAI.MaxCutGames.Integration.NoiseTables.Table
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.tableOutput_eq_with_witness line 187
Source documentation
The nonlinear correctness witness is erased from the output program.
```
theorem tableOutput_eq_with_witness (S : Source) (k : Nat) {s d : Nat}
    (T : Integration.NoiseTables.Table s d) (f : Ambient s d → Alphabet s)
    (hf : ∀ x c, f (x + (c, 0)) = f x + c) :
    tableOutput S k T = outputInstance S k (T.gadget f hf)
      (Integration.TableReduction.tableEnumeration T f hf) := by
…
```
Mentions: OAI.MaxCutGames.Integration.NoiseTables.Table, OAI.MaxCutGames.Decoder.TableKeysAddressGame.tableOutput, OAI.MaxCutGames.Decoder.TableKeysAddressGame.outputInstance, OAI.MaxCutGames.Integration.TableReduction.tableEnumeration
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.completeAt_tableOutput_iff line 194
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.soundAt_tableOutput_iff line 202
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.tableOutput_translations line 210
theorem OAI.MaxCutGames.Decoder.TableKeysAddressGame.vertexCount_eq_polynomial line 216
Source documentation
Exact polynomial capacity, without the legacy two-side factor.
```
theorem vertexCount_eq_polynomial (S : Source) (k s d : Nat) :
    vertexCount S k s d = (CanonicalAddress.capacityPolynomial k s d).eval
      (S.«variables» + S.occurrences) := by
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysAddressGame.vertexCount
theorem OAI.MaxCutGames.Decoder.MatrixGap.address_rate_eq_semantic_acceptance line 236

theorem OAI.MaxCutGames.Decoder.MatrixGap.address_value_le_of_semantic_acceptance line 264

Source documentation

Soundness is measured on the generated direct-address instance. Unused addresses and reindexing introduce no additional labeling advantage.

theorem address_value_le_of_semantic_acceptance (S : Source) (k : Nat) {s d : Nat}
    (T : NoiseTables.Table s d) (f : Ambient s d → Alphabet s)
    (hf : ∀ x c, f (x + (c, 0)) = f x + c)
    (h : ∀ labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s),
      TableKeysGame.acceptanceProbability S k (T.gadget f hf) labeling ≤ (99 : ℚ) / 100) :
    InstanceValue.value (TableKeysAddressGame.tableOutput S k T) ≤ (99 : ℝ) / 100 := by
…

Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.TableKeysGame.acceptanceProbability, OAI.MaxCutGames.Decoder.TableKeysAddressGame.tableOutput

theorem OAI.MaxCutGames.Decoder.MatrixGap.semantic_acceptance_le_address_value line 308
Source documentation
Every semantic labeling extends to a labeling of the padded address space. The generated edge list retains its exact acceptance fraction.
```
theorem semantic_acceptance_le_address_value (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (en : NoiseEnumeration g)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s)) :
    (TableKeysGame.acceptanceProbability S k g labeling : ℝ) ≤
      InstanceValue.value (TableKeysAddressGame.outputInstance S k g en) := by
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.TableKeysGame.acceptanceProbability, OAI.MaxCutGames.Decoder.TableKeysAddressGame.outputInstance

theorem OAI.MaxCutGames.Decoder.MatrixGap.address_value_ge_of_near_assignment line 335

Source documentation

The exact near-assignment loss and fair-bit factor one half, measured on the generated address instance and then cast to its real optimum value.

theorem address_value_ge_of_near_assignment (S : Source) (k : Nat) {s d : Nat}
    (T : NoiseTables.Table s d) (f : Ambient s d → Alphabet s)
    (hf : ∀ x c, f (x + (c, 0)) = f x + c)
    (assignment : Fin S.«variables» → Bool) (ξ p : ℚ)
    (hfailure : S.failure assignment ≤ ξ)
    (hstable : (T.gadget f hf).stabilityError ≤ p) :
    (1 : ℝ) - ((k : ℝ) * (ξ : ℝ) + (p : ℝ) / 2) ≤
      InstanceValue.value (TableKeysAddressGame.tableOutput S k T) := by
…

Mentions: OAI.MaxCutGames.Decoder.TableKeysAddressGame.tableOutput

structure OAI.MaxCutGames.Decoder.MatrixGap.Parameters line 373
Source documentation
Fixed matrix-test parameters, before the separate bipartite subdivision and repetition. Existence is proved by the v2 spectral/decoding argument.
```
structure Parameters (p : ℚ) where
…
```
theorem OAI.MaxCutGames.Decoder.MatrixGap.semantic_rate_le_address_value line 390
Source documentation
The rate of any semantic vertex labeling is realized on the direct address output. Isolated unused addresses receive an arbitrary valid label.
```
theorem semantic_rate_le_address_value (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (en : NoiseEnumeration g)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s)) :
    (GapSemantics.satisfactionRate (TableKeysGame.outputInstance S k g) labeling : ℝ) ≤
      InstanceValue.value (TableKeysAddressGame.outputInstance S k g en) := by
…
```
Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.TableKeysGame.outputInstance, OAI.MaxCutGames.Decoder.TableKeysAddressGame.outputInstance
def OAI.MaxCutGames.Decoder.MatrixGap.Parameters.output line 405
Source documentation
The actual output constructor depends only on finite tables, not on the correcting map or its equivariance proof.
```
def output (P : Parameters p) (S : Source) : Instance (2 ^ P.s) :=
…
```
Mentions: OAI.MaxCutGames.Decoder.MatrixGap.Parameters
theorem OAI.MaxCutGames.Decoder.MatrixGap.Parameters.completeness line 408
theorem OAI.MaxCutGames.Decoder.MatrixGap.Parameters.output_translations line 416