AtomicFiniteCertificate.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The finite interpolation blocks in An atomic certificate for triangular-lattice universal optimality are I−R and I+R. Their rational candidates have right residuals E=I−AB. The correction B+BE and a second-order remainder bound give the entrywise enclosures of the actual inverses.

lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.plusResidual_norm line 19
lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.minusResidual_norm line 25
theorem OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.sub_isUnit line 32
Source documentation
Both finite interpolation blocks are nonsingular.
```
theorem sub_isUnit : IsUnit (1 - RValue) :=
…
```
Mentions: OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.RValue
theorem OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.add_isUnit line 35
theorem OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.sub_inverse_two_sided line 38
theorem OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.add_inverse_two_sided line 43
lemma OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.inverseEnclosure_mem_of_bounds line 48
theorem OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.sub_inverse_enclosure line 60
Source documentation
The original corrected rational enclosure contains every inverse entry.
```
theorem sub_inverse_enclosure (i j : Fin 20) :
    (inverseEnclosure 0 i j).Mem ((1 - RValue)⁻¹ i j) := by
…
```
Mentions: OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.inverseEnclosure, OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.RValue
theorem OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.add_inverse_enclosure line 70

theorem OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.atomic_finite_certificate line 82

Source documentation

The six finite conclusions for the fixed twenty-dimensional atomic system.

theorem atomic_finite_certificate :
    IsUnit (1 - RValue) ∧
    IsUnit (1 + RValue) ∧
    ((1 - RValue) * (1 - RValue)⁻¹ = 1 ∧ (1 - RValue)⁻¹ * (1 - RValue) = 1) ∧
    ((1 + RValue) * (1 + RValue)⁻¹ = 1 ∧ (1 + RValue)⁻¹ * (1 + RValue) = 1) ∧
    (∀ i j, (inverseEnclosure 0 i j).Mem ((1 - RValue)⁻¹ i j)) ∧
    (∀ i j, (inverseEnclosure 1 i j).Mem ((1 + RValue)⁻¹ i j)) :=
…

Mentions: OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.RValue, OAI.AtomicTriangular.FiniteCertificate.AtomicMatrix.inverseEnclosure