OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceNormalizedSpectrum.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Literal source rounding and zero deletion feed the complete three-stage spin comparison. Only the source's upper coefficient and gap bounds are needed; a nonzero lower coefficient bound is proved by rounding.

  1. def OAI.ContinuumCoulomb.SourceNormalizedSpectrum.rounded line 14
  2. def OAI.ContinuumCoulomb.SourceNormalizedSpectrum.retained line 18
  3. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.rounded_bounded line 21
  4. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.retained_bounded line 26
  5. def OAI.ContinuumCoulomb.SourceNormalizedSpectrum.family line 29
  6. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.family_noLoops line 32
  7. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.rounded_matrix line 38
  8. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.family_matrix line 51
  9. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.family_bottom_error line 57
  10. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.family_bounds line 79
  11. theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.normalized_three_stage_bottom line 107

    Source documentation

    Full three-stage error after genuine source normalization, with no lower-weight hypothesis on the original published source.

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

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