ActualAlgebra.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The actual M48 algebra, its fixed defect pair, and its Cuntz dimension state.

theorem OAI.Kaplansky.partialSum_leftSquare_fin line 17
theorem OAI.Kaplansky.partialSum_rightSquare_fin line 23
abbrev OAI.Kaplansky.ActualDefectIndex line 41
abbrev OAI.Kaplansky.ActualDefectAlgebra line 42
instance OAI.Kaplansky.(instance at line 44) line 44
def OAI.Kaplansky.actualGeneratorNat line 52
theorem OAI.Kaplansky.actualGeneratorNat_column line 55
theorem OAI.Kaplansky.actualGeneratorNat_row line 59
def OAI.Kaplansky.actualDefectA line 67
def OAI.Kaplansky.actualDefectB line 68
theorem OAI.Kaplansky.actualDefectPair_spec line 72
Source documentation
The fixed pair in the actual 48-by-48 amplification satisfies the universal defect bound, without assuming that any quasitrace exists.
```
theorem actualDefectPair_spec :
    PositiveContraction actualDefectA ∧ PositiveContraction actualDefectB ∧
      ∀ τ : OneQuasitrace ActualDefectAlgebra, τ.Normalized →
        (1 : ℝ)/144 ≤ (τ (actualDefectA+actualDefectB) - τ actualDefectA - τ actualDefectB).re :=
…
```
Mentions: OAI.Kaplansky.PositiveContraction, OAI.Kaplansky.actualDefectA, OAI.Kaplansky.actualDefectB, OAI.Kaplansky.OneQuasitrace, OAI.Kaplansky.ActualDefectAlgebra
theorem OAI.Kaplansky.actualDefectAlgebra_separable line 78
def OAI.Kaplansky.actualDefectAmplificationEquiv line 84
Source documentation
Explicit matrix correspondence for every further amplification.
```
def actualDefectAmplificationEquiv (m : ℕ) :
    CStarMatrix (Fin m) (Fin m) ActualDefectAlgebra ≃⋆ₐ[ℂ]
      CStarMatrix (Fin (48*m)) (Fin (48*m)) ActualAlgebra :=
…
```
Mentions: OAI.Kaplansky.ActualDefectAlgebra, OAI.Kaplansky.ActualAlgebra
theorem OAI.Kaplansky.actualDefectAlgebra_matrix_not_properlyInfinite line 92
theorem OAI.Kaplansky.mainTarget_of_actualDefectQuasitrace line 98
theorem OAI.Kaplansky.actualCuntzDimensionState_nonempty line 109
Source documentation
An actual normalized dimension state exists for the constructed algebra. No quasitrace-existence premise, simplicity, or exactness assumption is used.
```
theorem actualCuntzDimensionState_nonempty : Nonempty (CuntzDimensionState ActualDefectAlgebra) :=
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.ActualDefectAlgebra
def OAI.Kaplansky.actualCuntzDimensionState line 113
Source documentation
A chosen state on actual Cuntz classes. No analytic correspondence is claimed.
```
def actualCuntzDimensionState : CuntzDimensionState ActualDefectAlgebra :=
…
```
Mentions: OAI.Kaplansky.CuntzDimensionState, OAI.Kaplansky.ActualDefectAlgebra
theorem OAI.Kaplansky.actualCuntzDimensionState_unit line 116