OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryLattice.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The actual sparse verifier compiler, through the specified planar lattice. The final precision pays for every early and routing error; the scalar offset is removed from both thresholds exactly.

  1. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.spatialDensity_pos line 19
  2. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.finalDensity_pos line 23
  3. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.iterate_count_ge line 25
  4. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.model_vertices_ge line 32
  5. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.model_vertices_pos line 43
  6. opaque OAI.ContinuumCoulomb.QuantumHistorySpatial.routeRoundValue line 53

    Source comment

    The certified value is fixed, but need never be expanded into a numeral.
    private opaque routeRoundValue : { k : ℕ //
    QMASpatialExchangeModel.routeLengthBound (spatialDensity rawDensity historyDegree)
      (27*spatialDensity rawDensity historyDegree) = k } :=
…

    Mentions: OAI.ContinuumCoulomb.QMASpatialExchangeModel.routeLengthBound, OAI.ContinuumCoulomb.QuantumHistorySpatial.rawDensity

  7. def OAI.ContinuumCoulomb.QuantumHistorySpatial.routeRounds line 59
  8. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.routeRounds_eq line 60
  9. def OAI.ContinuumCoulomb.QuantumHistorySpatial.totalRounds line 63
  10. def OAI.ContinuumCoulomb.QuantumHistorySpatial.latticePrecision line 64
  11. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.combine_errors line 66
  12. def OAI.ContinuumCoulomb.QuantumHistorySpatial.lattice line 71
  13. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.lattice_history_error line 76
  14. def OAI.ContinuumCoulomb.QuantumHistorySpatial.source line 94
  15. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.source_energy line 103
  16. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.source_accepting line 112
  17. theorem OAI.ContinuumCoulomb.QuantumHistorySpatial.source_rejecting line 129