BinaryWellCharges.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual rounded binary-well charges

The integer charges are fixed before the secondary displacement is tuned. Their normalized values satisfy explicit uniform smallness bounds, and their binary lengths remain linear in the geometric scale. This is analytic and encoding-size correctness. The charges themselves are computed by rational arithmetic. The isolated-energy tuning algorithm is separate.

def OAI.ContinuumCoulomb.binaryPrimaryCharge line 20
def OAI.ContinuumCoulomb.binarySecondaryCharge line 23
theorem OAI.ContinuumCoulomb.binaryPrimaryCharge_eq line 28
theorem OAI.ContinuumCoulomb.binarySecondaryCharge_eq line 33
def OAI.ContinuumCoulomb.binaryPrimaryRatio line 38
def OAI.ContinuumCoulomb.binarySecondaryRatio line 41
theorem OAI.ContinuumCoulomb.binaryWellCharges_spec line 44
theorem OAI.ContinuumCoulomb.binaryWellCharges_bit_length line 115

theorem OAI.ContinuumCoulomb.binary_isolatedPerturbation_bound line 133

Source documentation

Integer rounding of both actual physical charges preserves the isolated-well operator estimate uniformly throughout displacement tuning.

theorem binary_isolatedPerturbation_bound {D m : ℕ} (hm : 0 < m)
    (hscale : 2002 * m ≤ D) (center displacement : Fin m → Position)
    (hdisp : ∀ j, ‖displacement j‖ ≤ 4) (site : Fin m) (state : Coulomb.H1Vector 1) :
    (∑ spin, ∫ x, ‖(isolatedPerturbation (D : ℝ) (binaryPrimaryRatio D m)
      (binarySecondaryRatio D m) center displacement site (Coulomb.position x 0) : ℂ) *
        state.value spin x‖ ^ 2) ≤
      48 * (1001 * m / (D : ℝ)) ^ 2 * (Coulomb.kinetic state + Coulomb.mass state) := by
…

Mentions: OAI.ContinuumCoulomb.Position, OAI.Coulomb.H1Vector, OAI.ContinuumCoulomb.isolatedPerturbation, OAI.ContinuumCoulomb.binaryPrimaryRatio, OAI.ContinuumCoulomb.binarySecondaryRatio, OAI.Coulomb.position, OAI.Coulomb.kinetic, OAI.Coulomb.mass