TracialHalfProjectionData.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The centered reflection used by the dihedral test is constructed from a half-trace projection. Completing a smaller projection by an orthogonal projection of the complementary trace supplies that projection; no centered symmetry is assumed in this algebraic step.

theorem OAI.KadisonSimilarity.projectionReflection_eq_two_smul line 17
Source documentation
The existing ring reflection is exactly the desired scalar formula.
```
theorem projectionReflection_eq_two_smul (p : P) :
    projectionReflection p = (2 : ℂ) • p - 1 := by
…
```
Mentions: OAI.KadisonSimilarity.projectionReflection
theorem OAI.KadisonSimilarity.star_projectionReflection line 22
theorem OAI.KadisonSimilarity.projectionReflection_mul_self line 26
theorem OAI.KadisonSimilarity.dihedralHalfProjection_projectionReflection line 32
Source documentation
Taking the half projection of the constructed reflection recovers the original projection exactly.
```
@[simp] theorem dihedralHalfProjection_projectionReflection {p : P}
    (hp : IsStarProjection p) :
    dihedralHalfProjection (symmetryUnit (projectionReflection p)
      (projectionReflection_mul_self hp)) = p := by
…
```
Mentions: OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.symmetryUnit, OAI.KadisonSimilarity.projectionReflection, OAI.KadisonSimilarity.projectionReflection_mul_self
theorem OAI.KadisonSimilarity.projectionReflection_mul_of_support line 39
theorem OAI.KadisonSimilarity.mul_projectionReflection_of_support line 44

theorem OAI.KadisonSimilarity.halfProjection_support_of_support line 50

Source documentation

The exact half-projection identities consumed by the free-corner model.

theorem halfProjection_support_of_support {p e : P} (hp : IsStarProjection p)
    (hpe : p * e = e) (hep : e * p = e) :
    dihedralHalfProjection (symmetryUnit (projectionReflection p)
      (projectionReflection_mul_self hp)) * e = e ∧
    e * dihedralHalfProjection (symmetryUnit (projectionReflection p)
      (projectionReflection_mul_self hp)) = e := by
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.symmetryUnit, OAI.KadisonSimilarity.projectionReflection, OAI.KadisonSimilarity.projectionReflection_mul_self

theorem OAI.KadisonSimilarity.halfProjection_support_of_le line 63

Source documentation

Order containment of projections gives the two required support identities.

theorem halfProjection_support_of_le {p e : P} (hp : IsStarProjection p)
    (he : IsStarProjection e) (hep : e ≤ p) :
    dihedralHalfProjection (symmetryUnit (projectionReflection p)
      (projectionReflection_mul_self hp)) * e = e ∧
    e * dihedralHalfProjection (symmetryUnit (projectionReflection p)
      (projectionReflection_mul_self hp)) = e :=
…

Mentions: OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.symmetryUnit, OAI.KadisonSimilarity.projectionReflection, OAI.KadisonSimilarity.projectionReflection_mul_self

structure OAI.KadisonSimilarity.HalfTraceProjectionData line 77
Source documentation
Minimal half-projection data, before constructing the reflection. The existence of this data is supplied by projection completion in the intended finite factor; the next constructor derives it from an actual complement.
```
structure HalfTraceProjectionData (τ : P →ₗ[ℂ] ℂ) (e : P) where
…
```
def OAI.KadisonSimilarity.halfTraceProjectionDataOfOrthogonal line 86
Source documentation
Completing a small corner by an orthogonal complement of the missing trace produces a half-trace projection containing the original corner.
```
def halfTraceProjectionDataOfOrthogonal (τ : P →ₗ[ℂ] ℂ) {e q : P}
    (he : IsStarProjection e) (hq : IsStarProjection q) (heq : e * q = 0)
    {t : ℂ} (hetrace : τ e = t) (hqtrace : τ q = 1 / 2 - t) :
    HalfTraceProjectionData τ e where
…
```
Mentions: OAI.KadisonSimilarity.HalfTraceProjectionData
def OAI.KadisonSimilarity.HalfTraceProjectionData.reflection line 105
Source documentation
The actual centered reflection obtained from the completed projection.
```
def reflection : P := projectionReflection Q.projection
```
Mentions: OAI.KadisonSimilarity.projectionReflection
theorem OAI.KadisonSimilarity.HalfTraceProjectionData.reflection_star line 107
theorem OAI.KadisonSimilarity.HalfTraceProjectionData.reflection_square line 110
theorem OAI.KadisonSimilarity.HalfTraceProjectionData.reflection_trace line 113
theorem OAI.KadisonSimilarity.HalfTraceProjectionData.reflection_half line 118
Source documentation
Its half projection is the chosen completion, so all corner supports are the original concrete multiplication identities.
```
theorem reflection_half :
    dihedralHalfProjection (symmetryUnit Q.reflection Q.reflection_square) = Q.projection :=
…
```
Mentions: OAI.KadisonSimilarity.dihedralHalfProjection, OAI.KadisonSimilarity.symmetryUnit
theorem OAI.KadisonSimilarity.HalfTraceProjectionData.reflection_support line 122
theorem OAI.KadisonSimilarity.HalfTraceProjectionData.reflection_mul line 128