CanonicalAddress.lean`

59 declarations, 0 contain sorry, 0 declared as axioms

Direct canonical-body addresses. The fixed list of canonical words is interpreted in big-endian order, matching forward Horner steps B*acc+digit. Unused addresses represent isolated vertices. These are semantic encoding and polynomial-size results, not an assumed machine implementation.

def OAI.MaxCutGames.Reduction.CanonicalAddress.radix line 18
Source documentation
Most-significant-word first, with leading zero words retained in the fixed-length domain. Mathlib's ofDigits uses the opposite list order.
```
def radix (B : Nat) (words : List Nat) : Nat := Nat.ofDigits B words.reverse
```
theorem OAI.MaxCutGames.Reduction.CanonicalAddress.radix_eq_foldl line 20
theorem OAI.MaxCutGames.Reduction.CanonicalAddress.radix_nil line 26
theorem OAI.MaxCutGames.Reduction.CanonicalAddress.radix_append_word line 29
Source documentation
This is precisely the arithmetic operation of MachineRadixStep.
```
theorem radix_append_word (B : Nat) (words : List Nat) (digit : Nat) :
    radix B (words ++ [digit]) = B * radix B words + digit := by
…
```
Mentions: OAI.MaxCutGames.Reduction.CanonicalAddress.radix
theorem OAI.MaxCutGames.Reduction.CanonicalAddress.radix_lt_pow_length line 33

theorem OAI.MaxCutGames.Reduction.CanonicalAddress.radix_injective_of_length_eq line 41

Source documentation

Fixed width makes leading zero words unambiguous.

theorem radix_injective_of_length_eq {B : Nat} (hB : 1 < B)
    {xs ys : List Nat} (sameLength : xs.length = ys.length)
    (xsBounded : ∀ w ∈ xs, w < B) (ysBounded : ∀ w ∈ ys, w < B)
    (sameAddress : radix B xs = radix B ys) : xs = ys := by
…

Mentions: OAI.MaxCutGames.Reduction.CanonicalAddress.radix

def OAI.MaxCutGames.Reduction.CanonicalAddress.base line 53
Source documentation
One larger than the proved bound on every canonical word.
```
def base (n m s d : Nat) : Nat := wordBound n m s d + 1
```
theorem OAI.MaxCutGames.Reduction.CanonicalAddress.base_eq line 55
theorem OAI.MaxCutGames.Reduction.CanonicalAddress.one_lt_base line 59
theorem OAI.MaxCutGames.Reduction.CanonicalAddress.bodyWords_lt_base line 66
def OAI.MaxCutGames.Reduction.CanonicalAddress.capacity line 70
theorem OAI.MaxCutGames.Reduction.CanonicalAddress.capacity_pos line 72
def OAI.MaxCutGames.Reduction.CanonicalAddress.bodyAddress line 75
theorem OAI.MaxCutGames.Reduction.CanonicalAddress.bodyAddress_val line 81
theorem OAI.MaxCutGames.Reduction.CanonicalAddress.bodyAddress_injective line 84
theorem OAI.MaxCutGames.Reduction.CanonicalAddress.bodyAddress_eq_iff line 92
def OAI.MaxCutGames.Reduction.CanonicalAddress.capacityPolynomial line 96
Source documentation
For fixed k,s,d, the entire direct-address space is a polynomial in n+m.
```
noncomputable def capacityPolynomial (k s d : Nat) : Polynomial Nat :=
…
```
theorem OAI.MaxCutGames.Reduction.CanonicalAddress.capacityPolynomial_eval line 99
def OAI.MaxCutGames.Integration.NoiseTables.reindex line 115
Source documentation
Reindexing changes the names of outcomes, retaining their uniform law.
```
def reindex (g : SplitGadget s d) {I : Type} [Fintype I] [Nonempty I]
    (e : I ≃ g.NoiseIndex) : SplitGadget s d where
…
```
theorem OAI.MaxCutGames.Integration.NoiseTables.reindex_stabilityError line 124
theorem OAI.MaxCutGames.Integration.NoiseTables.reindex_kernelProbability line 131
structure OAI.MaxCutGames.Integration.NoiseTables.Table line 144
Source documentation
Only a nonempty finite list of binary vectors is required as static noise data. The correcting function is a separate witness used in the proof.
```
structure Table (s d : Nat) where
…
```
def OAI.MaxCutGames.Integration.NoiseTables.Table.gadget line 150
def OAI.MaxCutGames.Integration.NoiseTables.Table.ofEnumeration line 159
theorem OAI.MaxCutGames.Integration.NoiseTables.Table.ofEnumeration_length line 163
def OAI.MaxCutGames.Integration.NoiseTables.Table.positionEquiv line 169
Source documentation
The inverse equivalence is used only to prove the probability identity; the forward noise lookup is ordinary finite-list indexing.
```
noncomputable def positionEquiv (g : SplitGadget s d) (en : NoiseEnumeration g) :
    Fin (ofEnumeration g en).vectors.length ≃ g.NoiseIndex := by
…
```
Mentions: OAI.MaxCutGames.Integration.NoiseTables.Table.ofEnumeration
theorem OAI.MaxCutGames.Integration.NoiseTables.Table.noise_positionEquiv line 175
theorem OAI.MaxCutGames.Integration.NoiseTables.Table.stabilityError_ofEnumeration line 182
theorem OAI.MaxCutGames.Integration.NoiseTables.Table.kernelProbability_ofEnumeration line 192

theorem OAI.MaxCutGames.Integration.NoiseTables.Table.guarantees_ofEnumeration line 203

Source documentation

Exact table conversion retains both mathematical gadget guarantees.

theorem guarantees_ofEnumeration (g : SplitGadget s d) (en : NoiseEnumeration g)
    {ζ ν : ℚ} {r : Nat}
    (hstable : g.stabilityError ≤ ζ)
    (hdisp : ∀ (P : Type) [AddCommGroup P] [Module F2 P]
      (S : Ambient s d →ₗ[F2] P),
      r ≤ Module.finrank F2 (S.comp (alphabetEmbedding s d)).range →
      SplitGadget.kernelProbability g S ≤ ν) :
    ((ofEnumeration g en).gadget g.f g.equivariant).stabilityError ≤ ζ ∧
      ∀ (P : Type) [AddCommGroup P] [Module F2 P]
        (S : Ambient s d →ₗ[F2] P),
        r ≤ Module.finrank F2 (S.comp (alphabetEmbedding s d)).range →
        SplitGadget.kernelProbability
…

Mentions: OAI.MaxCutGames.Integration.SplitGadget.kernelProbability, OAI.MaxCutGames.Integration.NoiseTables.Table.ofEnumeration, OAI.MaxCutGames.Integration.NoiseTables.Table.gadget

def OAI.MaxCutGames.Integration.TableReduction.tableEnumeration line 232
def OAI.MaxCutGames.Integration.TableReduction.tableSkeleton line 240
Source documentation
The projection is used only to fill an erased witness field. It is never used when generating constraints or evaluating their permutation tables.
```
def tableSkeleton (T : Table s d) : SplitGadget s d :=
…
```
def OAI.MaxCutGames.Integration.TableReduction.output line 244
Source documentation
A total executable map with finite vector data and no nonlinear-map input.
```
def output (S : Source) (k : Nat) (T : Table s d) : Instance (2 ^ s) :=
…
```
theorem OAI.MaxCutGames.Integration.TableReduction.output_eq_with_witness line 250
Source documentation
Every correcting-map witness generates exactly the same numbered instance, including the ordered constraint list and all permutation entries.
```
theorem output_eq_with_witness (S : Source) (k : Nat) (T : Table s d)
    (f : Ambient s d → Alphabet s) (hf : ∀ x c, f (x + (c, 0)) = f x + c) :
    output S k T =
      outputInstanceWithEnumeration S k (T.gadget f hf) (tableEnumeration T f hf) := by
…
```
Mentions: OAI.MaxCutGames.Integration.TableReduction.output, OAI.MaxCutGames.Integration.TableReduction.tableEnumeration
theorem OAI.MaxCutGames.Integration.TableReduction.completeAt_output_iff line 256
theorem OAI.MaxCutGames.Integration.TableReduction.soundAt_output_iff line 264
theorem OAI.MaxCutGames.Integration.TableReduction.edge_ofEnumeration line 272
theorem OAI.MaxCutGames.Integration.TableReduction.acceptance_ofEnumeration line 280
theorem OAI.MaxCutGames.Integration.TableReduction.rate_ofEnumeration line 292
theorem OAI.MaxCutGames.Integration.TableReduction.completeAt_ofEnumeration_iff line 303
Source documentation
Normalization to a concrete table preserves the original completeness threshold exactly; there is no additional approximation loss.
```
theorem completeAt_ofEnumeration_iff (error : RationalError)
    (S : Source) (k : Nat) (g : SplitGadget s d) (en : NoiseEnumeration g) :
    CompleteAt error (output S k (Table.ofEnumeration g en)) ↔
      CompleteAt error (outputInstance S k g) := by
…
```
Mentions: OAI.MaxCutGames.Integration.TableReduction.output
theorem OAI.MaxCutGames.Integration.TableReduction.soundAt_ofEnumeration_iff line 315
def OAI.MaxCutGames.Integration.VertexEmbedding.embedConstraint line 338
theorem OAI.MaxCutGames.Integration.VertexEmbedding.embedConstraint_satisfied line 344
theorem OAI.MaxCutGames.Integration.VertexEmbedding.embedConstraint_permutation line 348
theorem OAI.MaxCutGames.Integration.VertexEmbedding.count_map line 351
def OAI.MaxCutGames.Integration.VertexEmbedding.embedInstance line 360
theorem OAI.MaxCutGames.Integration.VertexEmbedding.embedInstance_vertices line 366
theorem OAI.MaxCutGames.Integration.VertexEmbedding.embedInstance_constraints line 370
theorem OAI.MaxCutGames.Integration.VertexEmbedding.embedInstance_length line 374
theorem OAI.MaxCutGames.Integration.VertexEmbedding.count_embed line 378
theorem OAI.MaxCutGames.Integration.VertexEmbedding.satisfactionRate_embed line 384
def OAI.MaxCutGames.Integration.VertexEmbedding.extendLabeling line 393
Source documentation
The extension is only used as a semantic witness, not by the instance constructor.
```
noncomputable def extendLabeling {n m q : Nat} (f : Fin n → Fin m)
    (labeling : Fin n → Fin q) (defaultLabel : Fin q) (v : Fin m) : Fin q := by
…
```
theorem OAI.MaxCutGames.Integration.VertexEmbedding.extendLabeling_apply line 398
theorem OAI.MaxCutGames.Integration.VertexEmbedding.extendLabeling_comp line 407
theorem OAI.MaxCutGames.Integration.VertexEmbedding.soundAt_embed line 413
theorem OAI.MaxCutGames.Integration.VertexEmbedding.completeAt_embed line 421
theorem OAI.MaxCutGames.Integration.VertexEmbedding.completeAt_embed_iff line 429
theorem OAI.MaxCutGames.Integration.VertexEmbedding.soundAt_embed_iff line 439
theorem OAI.MaxCutGames.Integration.VertexEmbedding.isTranslationInstance_embed_iff line 448