SourceNormalizedLattice.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Literal coefficient rounding and zero deletion preserve the original square-lattice geometry and the simple unordered edge enumeration.

theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.rounded_injective line 13
theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.retained_nodup line 22
theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.family_original_edge line 27
Source documentation
Every retained bond has the same two endpoints as a definite original source bond; only its coefficient has been rounded.
```
theorem family_original_edge (d : SquareLatticeHeisenberg) (M : ℕ)
    (e : Fin (retained d M).length) :
    ∃ i : Fin d.edges, (family d M).left e = d.left i ∧
      (family d M).right e = d.right i ∧
      (retained d M).get e = ((d.left i).val, (d.right i).val,
        SourceCoefficientRounding.coefficient M (d.coefficient i)) := by
…
```
Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.SourceNormalizedSpectrum.retained, OAI.ContinuumCoulomb.SourceNormalizedSpectrum.family, OAI.ContinuumCoulomb.SourceCoefficientRounding.coefficient
theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.family_adjacent line 38
theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.family_edge_simple line 48
def OAI.ContinuumCoulomb.SourceNormalizedSpectrum.lattice line 70
Source documentation
The normalized graph in the same geometric source type. Its thresholds are inherited only to satisfy the record; all coefficient and matrix normalization theorems continue to use the literal family definition.
```
def lattice (d : SquareLatticeHeisenberg) (M : ℕ) : SquareLatticeHeisenberg where
…
```
Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg
theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.lattice_bonds line 85
theorem OAI.ContinuumCoulomb.SourceNormalizedSpectrum.lattice_coordinate line 88