PreprocessingTableSpectral.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Spectral certificates for the actual materialized preprocessing tables. Exact rotation identities transport the checked semantic overlay and lazy estimates to the stored tables. No spectral premise is imposed on the original constraint table in the overlay theorem.

theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTableSpectral.portGraph_ext line 19
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTableSpectral.materialize_portGraph line 28
Source documentation
Materialization retains exactly the explicitly reindexed rotation.
```
theorem materialize_portGraph {n d : Nat} {D : Type*}
    (G : ConstraintGraph (Fin n) (Fin n × D) PortTables.Label)
    (ports : D ≃ Fin d) :
    PortTables.portGraph (PreprocessingOverlayTables.materialize G ports) =
      GraphTransport.reindex (Overlay.originalPortGraph G) (Equiv.refl _) ports := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Label, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.materialize, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTransport.reindex, OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.originalPortGraph
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTableSpectral.overlay_portGraph line 40
Source documentation
The stored overlaid graph is the actual semantic overlay in numbered port coordinates. This is equality of reversible port graphs.
```
theorem overlay_portGraph {n d e : Nat} (G : PortTables.Table n d)
    (H : ExpanderTables.Table n e) :
    PortTables.portGraph (PreprocessingOverlayTables.overlay G H) =
      GraphTransport.reindex
        (Overlay.portGraph (PortTables.portGraph G) (ExpanderTables.graph H))
        (Equiv.refl _) (PreprocessingOverlayTables.overlayPorts d e) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.overlay, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTransport.reindex, OAI.UniqueGamesTheorem.Foundations.PCP.Overlay.portGraph, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.graph, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.overlayPorts
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTableSpectral.overlay_rotation_eq line 50
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTableSpectral.lazy_portGraph line 61
Source documentation
The stored lazy graph is exactly the Boolean-flag lazy graph, with the declared false-first port encoding.
```
theorem lazy_portGraph {n d : Nat} (G : PortTables.Table n d) :
    PortTables.portGraph (PreprocessingOverlayTables.lazy G) =
      GraphTransport.reindex (lazyGraph (PortTables.portGraph G))
        (Equiv.refl _) (PreprocessingOverlayTables.lazyPorts d) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazy, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTransport.reindex, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazyPorts
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTableSpectral.lazy_rotation_eq line 69
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTableSpectral.overlay_certificate_seven_eighths line 80
Source documentation
An actual half-spectral expander overlay gives a 7/8 certificate for the stored table. The original table needs no spectral certificate. The degree hypothesis supplies nonempty old and expander port types.
```
theorem overlay_certificate_seven_eighths {n d e : Nat}
    (G : PortTables.Table n d) (H : ExpanderTables.Table n e)
    (hn : 0 < n) (hdegree : d = e + 1) (he : 8 ≤ e)
    (hH : SpectralCertificate (ExpanderTables.graph H) (1 / 2 : ℝ)) :
    SpectralCertificate (PortTables.portGraph (PreprocessingOverlayTables.overlay G H))
      (7 / 8 : ℝ) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderTables.graph, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.overlay
theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTableSpectral.lazy_certificate_31_32 line 98
Source documentation
An actual 7/8 certificate gives a 31/32 certificate for the materialized lazy table. Only the original port set must be nonempty.
```
theorem lazy_certificate_31_32 {n d : Nat} (G : PortTables.Table n d)
    (hd : 0 < d) (hG : SpectralCertificate (PortTables.portGraph G) (7 / 8 : ℝ)) :
    SpectralCertificate (PortTables.portGraph (PreprocessingOverlayTables.lazy G))
      (31 / 32 : ℝ) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.portGraph, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingOverlayTables.lazy