SourceConditionalReduction.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A polynomial-time source-to-unit-Coulomb reduction under explicit analytic hypotheses.

theorem OAI.ContinuumCoulomb.exists_source_unit_reduction_with_planar_gap line 22
theorem OAI.ContinuumCoulomb.exists_source_unit_reduction_without_hydrogen line 162
Source documentation
The planar spectral hypothesis implies the estimate for the manufactured well.
```
theorem exists_source_unit_reduction_without_hydrogen
    (hflow : PublishedC4FlowInput)
    (hp : PlanarSobolev.PublishedNegativePlanarGroundGap)
    (hv : PublishedVerticalOscillatorGap) (hdensity : PublishedSobolevSmoothDensity)
    (s : ℕ) :
    Nonempty (PolynomialManyOne binaryHeisenbergCodec.encode unitCoulombCodec.encode
      (sourceHeisenbergPromise s) unitCoulombPromise) :=
…
```
Mentions: OAI.ContinuumCoulomb.PublishedC4FlowInput, OAI.ContinuumCoulomb.PlanarSobolev.PublishedNegativePlanarGroundGap, OAI.ContinuumCoulomb.PublishedVerticalOscillatorGap, OAI.ContinuumCoulomb.PublishedSobolevSmoothDensity, OAI.ContinuumCoulomb.PolynomialManyOne, OAI.ContinuumCoulomb.sourceHeisenbergPromise, OAI.ContinuumCoulomb.unitCoulombPromise
theorem OAI.ContinuumCoulomb.exists_source_unit_reduction line 173
Source documentation
A six-hypothesis form of the reduction, including the hydrogen spectral hypothesis.
```
theorem exists_source_unit_reduction
    (hflow : PublishedC4FlowInput)
    (hp : PlanarSobolev.PublishedNegativePlanarGroundGap)
    (hv : PublishedVerticalOscillatorGap) (hdensity : PublishedSobolevSmoothDensity)
    (_hh : PublishedHydrogenBottom) (s : ℕ) :
    Nonempty (PolynomialManyOne binaryHeisenbergCodec.encode unitCoulombCodec.encode
      (sourceHeisenbergPromise s) unitCoulombPromise) :=
…
```
Mentions: OAI.ContinuumCoulomb.PublishedC4FlowInput, OAI.ContinuumCoulomb.PlanarSobolev.PublishedNegativePlanarGroundGap, OAI.ContinuumCoulomb.PublishedVerticalOscillatorGap, OAI.ContinuumCoulomb.PublishedSobolevSmoothDensity, OAI.ContinuumCoulomb.PublishedHydrogenBottom, OAI.ContinuumCoulomb.PolynomialManyOne, OAI.ContinuumCoulomb.sourceHeisenbergPromise, OAI.ContinuumCoulomb.unitCoulombPromise