OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedTensorGap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed positive gap on the actual full-domain tensor complement. The only analytic inputs are the published planar, oscillator and density statements; the finite tensor projection and its occupation deficit are proved.

  1. theorem OAI.ContinuumCoulomb.manufacturedSlab_uniform_tensorComplement_gap line 15