OAI/Computability/UniqueGames/Reduction/OutputSize.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Polynomial encoded length of the actual output

The encoder is the foundations team's unary, delimited forward-permutation format. The instance is the actual list-based reduction, including canonical body deduplication and every repeated edge occurrence. The polynomial's coefficients depend only on the fixed gadget table and tuple dimensions.

These are output-length theorems. They do not assert a machine running-time certificate for canonicalization, enumeration, or serialization.

  1. theorem OAI.UniqueGamesTheorem.Reduction.OutputSize.explicitBodies_length_le line 30
  2. def OAI.UniqueGamesTheorem.Reduction.OutputSize.vertexCoefficient line 39
  3. def OAI.UniqueGamesTheorem.Reduction.OutputSize.edgeCoefficient line 42
  4. theorem OAI.UniqueGamesTheorem.Reduction.OutputSize.collect_vertex_coefficient line 46
  5. theorem OAI.UniqueGamesTheorem.Reduction.OutputSize.collect_edge_coefficient line 51
  6. theorem OAI.UniqueGamesTheorem.Reduction.OutputSize.output_vertices_le line 56
  7. theorem OAI.UniqueGamesTheorem.Reduction.OutputSize.output_constraints_eq line 70
  8. def OAI.UniqueGamesTheorem.Reduction.OutputSize.sizeBound line 77
  9. theorem OAI.UniqueGamesTheorem.Reduction.OutputSize.sizeBound_mono line 83
  10. theorem OAI.UniqueGamesTheorem.Reduction.OutputSize.output_bits_length_le line 95
  11. def OAI.UniqueGamesTheorem.Reduction.OutputSize.outputPolynomial line 110

    Source documentation

    An explicit polynomial for the actual serialized game.

    noncomputable def outputPolynomial (k : Nat) (T : NoiseTables.Table s d) : Polynomial Nat :=
…
  12. theorem OAI.UniqueGamesTheorem.Reduction.OutputSize.outputPolynomial_eval line 116
  13. theorem OAI.UniqueGamesTheorem.Reduction.OutputSize.output_bits_polynomial_in_occurrences line 121
  14. theorem OAI.UniqueGamesTheorem.Reduction.OutputSize.output_bits_polynomial_in_input line 129
  15. theorem OAI.UniqueGamesTheorem.Reduction.OutputSize.fixed_parameters_output_size line 139

    Source documentation

    Fixed reduction parameters give one polynomial for every encoded input.

    theorem fixed_parameters_output_size (k : Nat) (T : NoiseTables.Table s d) :
    ∃ p : Polynomial Nat, ∀ input : SourceEncoding.Input,
      (Complexity.gameBits
        (UniformReduction.output input.equations input.nonempty k T)).length ≤
          p.eval (SourceEncoding.inputBits input).length :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.SourceEncoding.Input, OAI.UniqueGamesTheorem.Reduction.UniformReduction.output, OAI.UniqueGamesTheorem.Reduction.SourceEncoding.inputBits