RoundSize.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Size of the actual fixed amplification round

All constants below depend only on the fixed port alphabet and walk length. The round itself is the checked preprocessing, powering, and alphabet graph construction in AmplificationRound; no second graph constructor is introduced. Closed constants are kept symbolic rather than evaluated.

theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.card_padded_alphabet line 23
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.card_powered_dart line 30
opaque OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.lockedNat line 41
Source comment
An opaque value with a checked equality prevents the kernel's closed-numeral evaluator from expanding the astronomical powers. Its body is proved once for an arbitrary natural number; no axiom or trusted evaluator is introduced. Only size bounds use these constants, not the graph's algorithm definitions.
```
private opaque lockedNat (n : Nat) : {m : Nat // m = n} := ⟨n, rfl⟩
```
def OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.poweredAlphabetSize line 43
def OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.poweredDartFactor line 47
def OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.sizeFactor line 50
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.poweredAlphabetSize_eq line 54
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.poweredDartFactor_eq line 58
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.sizeFactor_eq line 62
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.coefficient_positive line 66
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.poweredAlphabet_card line 71
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.sizeFactor_positive line 80
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.factor_total line 86
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.nat_card_output_vertex line 89
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.nat_card_output_dart line 97
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.nat_card_output_total_le line 104
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.poweredDart_card line 116
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.output_vertex_card line 127
Source documentation
The exact cardinality of the round's output vertex type.
```
theorem output_vertex_card (G : ConstraintGraph V E AmplificationRound.Label) :
    Fintype.card (AmplificationRound.Vertex G) =
      Fintype.card (Preprocessing.Vertex G) * 2 ^ poweredAlphabetSize +
        (Fintype.card (Preprocessing.Vertex G) * poweredDartFactor) *
          AlphabetGraphBounds.vertexFactor poweredAlphabetSize := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.poweredAlphabetSize, OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.poweredDartFactor, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.vertexFactor
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.output_dart_card line 142
Source documentation
The exact cardinality of the round's output dart type.
```
theorem output_dart_card (G : ConstraintGraph V E AmplificationRound.Label) :
    Fintype.card (AmplificationRound.Dart G) =
      (Fintype.card (Preprocessing.Vertex G) * poweredDartFactor) *
        AlphabetGraphBounds.dartFactor poweredAlphabetSize := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.Dart, OAI.UniqueGamesTheorem.Foundations.PCP.Preprocessing.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.poweredDartFactor, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetGraphBounds.dartFactor, OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.poweredAlphabetSize
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.output_total_le_darts line 154
Source documentation
The actual round has linear total size, even in the old dart count alone.
```
theorem output_total_le_darts (G : ConstraintGraph V E AmplificationRound.Label) :
    Fintype.card (AmplificationRound.Vertex G) + Fintype.card (AmplificationRound.Dart G) ≤
      sizeFactor * Fintype.card E := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.ConstraintGraph, OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.Label, OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.Vertex, OAI.UniqueGamesTheorem.Foundations.PCP.AmplificationRound.Dart, OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.sizeFactor
theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundSize.output_total_le line 180