PreprocessingRegularSoundness.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Soundness of the executable regularization tables

The fixed input base table is required only to have its proved spectral certificate. Every positive cloud uses the actual recursively generated table at its computed size. Its spectral certificate gives the precise cut bound used by majority rounding. Empty clouds are handled by their zero cardinality. Thus neither expansion nor the desired count comparison is an input premise.

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.internalDegree_ge_eight line 23
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.baseDegree_ne_zero line 27
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.resizeTable_certificate line 34
Source documentation
Erasing a proof-equal table size preserves its exact spectral certificate.
```
theorem resizeTable_certificate {n m q : Nat} (h : n = m)
    (table : ExpanderTables.Table n q) (lambda : ℝ)
    (certificate : SpectralCertificate (ExpanderTables.graph table) lambda) :
    SpectralCertificate (ExpanderTables.graph (resizeTable h table)) lambda := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.graph
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.familyCloudTable_certificate_of_pos line 41
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.cloudGraphs_certificate_of_pos line 52

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.cloud_expansion line 62

Source documentation

The exact finite cut inequality needed to pay for each changed cloud label.

theorem cloud_expansion (H : BaseTable)
    (certificate : SpectralCertificate (ExpanderTables.graph H) (1 / 100 : ℝ))
    (t : GraphTables.Table) (v : Fin t.vertices)
    (S : Finset (PreprocessingCloudIndex.PaddedCloud t (padding t) v))
    (hsmall : S.card ≤
      Fintype.card (PreprocessingCloudIndex.PaddedCloud t (padding t) v) / 2) :
    2 * S.card ≤ (CloudRounding.directedCut
      (fun ed => ((cloudGraphs t (padding t) (familyCloudTable H t) v).rot ed).1) S).card := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.graph, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingCloudIndex.PaddedCloud, OAI.UniqueGamesTheorem.Foundations.PCP.CloudRounding.directedCut

def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.roundLabels line 85
Source documentation
Decode the actual numbered output labels by majority in each padded cloud.
```
noncomputable def roundLabels (t : GraphTables.Table)
    (labels : Fin (vertexCount t (padding t)) → GraphTables.Label) :
    Fin t.vertices → GraphTables.Label :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.soundness line 93
Source documentation
Direct soundness for the generated tables, with no matching-base premise.
```
theorem soundness (H : BaseTable)
    (certificate : SpectralCertificate (ExpanderTables.graph H) (1 / 100 : ℝ))
    (t : GraphTables.Table)
    (labels : Fin (vertexCount t (padding t)) → GraphTables.Label) :
    (GraphTables.semantics t).rejectionCount (roundLabels t labels) ≤
      (PortTables.baseGraph (regularize H t)).rejectionCount labels := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.graph, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.roundLabels, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.baseGraph
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.exists_rounding line 104
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.lift_rejectionCount line 114
Source documentation
Completeness preserves the number of rejected original dart occurrences.
```
theorem lift_rejectionCount (H : BaseTable) (t : GraphTables.Table)
    (labels : Fin t.vertices → GraphTables.Label) :
    (PortTables.baseGraph (regularize H t)).rejectionCount
        (liftedLabel t (padding t) labels) = (GraphTables.semantics t).rejectionCount labels :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.baseGraph, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.semantics
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.completeness line 120
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_lower_bound line 142
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_real_lower_bound line 151