OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceNormalizedPromise.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A fixed polynomial common denominator absorbs both coefficient rounding and all three mediator errors into one inverse-polynomial promise budget.

  1. def OAI.ContinuumCoulomb.SourceNormalizedSpectrum.denominator line 11
  2. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.denominator_pos line 13
  3. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.normalization_budget line 17
  4. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.source_positive_bottom line 35

    Source documentation

    The original source permits arbitrarily small and zero rational coefficients. This complete positive-spin comparison does too.

    theorem source_positive_bottom (d : SquareLatticeHeisenberg) {W G : ℕ}
    (hG : 0 < G) (hW : ∀ e, |(d.coefficient e : ℝ)| ≤ W) :
    |sourceMatrixBottom
      (d.vertices + (retained d (denominator d.edges G)).length * 2 +
        (retained d (denominator d.edges G)).length * 2 * 2 +
        ((retained d (denominator d.edges G)).length * 2 +
          (retained d (denominator d.edges G)).length * 2 * 2) * 2)
      (MediatorIteration.finalGraph (family d (denominator d.edges G))
        (denominator d.edges G + W + 1) G).matrix +
      (MediatorIteration.offset (family d (denominator d.edges G))
        (denominator d.edges G + W + 1) G : ℝ) - realSourceGroundEnergy d| ≤
      1 / (128 * (G : ℝ)) :=
…

    Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.sourceMatrixBottom, OAI.ContinuumCoulomb.SourceNormalizedSpectrum.retained, OAI.ContinuumCoulomb.SourceNormalizedSpectrum.denominator, OAI.ContinuumCoulomb.MediatorIteration.finalGraph, OAI.ContinuumCoulomb.SourceNormalizedSpectrum.family, OAI.ContinuumCoulomb.MediatorIteration.offset, OAI.ContinuumCoulomb.realSourceGroundEnergy

  5. def OAI.ContinuumCoulomb.SourceNormalizedSpectrum.lowerThreshold line 50
  6. def OAI.ContinuumCoulomb.SourceNormalizedSpectrum.upperThreshold line 54
  7. def OAI.ContinuumCoulomb.SourceNormalizedSpectrum.positiveEnergy line 58
  8. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.source_positive_yes line 63
  9. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.source_positive_no line 73
  10. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.positive_threshold_gap line 83