OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourcePositiveBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual source normalization and metadata programs give one fixed polynomial coefficient exponent for the final positive-spin graph.

  1. abbrev OAI.ContinuumCoulomb.SourceMetadataProgram.finalBound line 17
  2. opaque OAI.ContinuumCoulomb.SourceMetadataProgram.normalizedEnvironmentProgram line 23
  3. opaque OAI.ContinuumCoulomb.SourceMetadataProgram.finalBoundProgram line 27
  4. theorem OAI.ContinuumCoulomb.SourceMetadataProgram.finalBound_power line 32
  5. theorem OAI.ContinuumCoulomb.SourceMetadataProgram.envWeight_congr line 36
  6. theorem OAI.ContinuumCoulomb.SourceMetadataProgram.finalBound_of_env line 42
  7. theorem OAI.ContinuumCoulomb.SourceMetadataProgram.finalBound_eq line 47
  8. theorem OAI.ContinuumCoulomb.SourceMetadataProgram.retained_count_le line 59
  9. theorem OAI.ContinuumCoulomb.SourceMetadataProgram.positive_graph_count_bound line 67
  10. theorem OAI.ContinuumCoulomb.SourceMetadataProgram.source_positive_weight_range line 79

    Source documentation

    One fixed exponent controls every final coefficient, even when the original source contains zero or exponentially tiny rational coefficients.

    theorem source_positive_weight_range (k : ℕ) :
    ∃ A : ℕ, 0 < A ∧ ∀ (d : BinaryHeisenberg) (h : d.Valid),
      d.PolynomialPromise k → ∀ e,
      (((binaryHeisenbergCodec.encode d).length + 2 : ℝ) ^ A)⁻¹ ≤
        ((MediatorIteration.finalGraph
          (SourceNormalizedSpectrum.family (d.toSource h) (roundingDenominator k d))
          (roundingDenominator k d + size d ^ k + 1) (size d ^ k)).weight e : ℝ) ∧
      ((MediatorIteration.finalGraph
          (SourceNormalizedSpectrum.family (d.toSource h) (roundingDenominator k d))
          (roundingDenominator k d + size d ^ k + 1) (size d ^ k)).weight e : ℝ) ≤
        ((binaryHeisenbergCodec.encode d).length + 2 : ℝ) ^ A := by
…

    Mentions: OAI.ContinuumCoulomb.BinaryHeisenberg, OAI.ContinuumCoulomb.MediatorIteration.finalGraph, OAI.ContinuumCoulomb.SourceNormalizedSpectrum.family, OAI.ContinuumCoulomb.SourceMetadataProgram.roundingDenominator, OAI.ContinuumCoulomb.SourceMetadataProgram.size