Complement.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Regrouping retained frames and their complement bundles.

def OAI.Kaplansky.ContinuousOrthonormalStageFrame.congr line 20
def OAI.Kaplansky.retainedGroupedStage line 28
theorem OAI.Kaplansky.properlyInfinite_regrouped_frame line 34
Source documentation
The polynomial image frame is transported to the actual line-bundle presentation used in the Chern computation. No characteristic-class nonvanishing or obstruction is a premise.
```
theorem properlyInfinite_regrouped_frame {m : ℕ} (hm : 0<m)
    (hpi : ProperlyInfinite (CStarMatrix (Fin m) (Fin m) ActualAlgebra)) :
    ∃ R : ℕ, 0<R ∧ Nonempty (ContinuousOrthonormalStageFrame (retainedGroupedStage m R)
      (2*m*testRank m R 0)) := by
…
```
Mentions: OAI.Kaplansky.ProperlyInfinite, OAI.Kaplansky.ActualAlgebra, OAI.Kaplansky.ContinuousOrthonormalStageFrame, OAI.Kaplansky.retainedGroupedStage, OAI.Kaplansky.testRank
theorem OAI.Kaplansky.properlyInfinite_retained_complement line 44
Source documentation
A hypothetical proper-infiniteness witness yields a genuine continuous frame whose orthogonal complement has rank below the Chern degree on every fiber. Identifying that Chern class and proving it nonzero remain separate.
```
theorem properlyInfinite_retained_complement {m : ℕ} (hm : 0<m)
    (hpi : ProperlyInfinite (CStarMatrix (Fin m) (Fin m) ActualAlgebra)) :
    ∃ (R : ℕ) (_ : 0<R) (f : ContinuousOrthonormalStageFrame (retainedLineStage m R)
      (2*m*testRank m R 0)),
      ∀ y : SmoothTestBase m R,
        Module.finrank ℂ (Submodule.span ℂ (Set.range (f.vector y)))ᗮ <
          ∑ i : Fin R, testProjectiveDimension m R i := by
…
```
Mentions: OAI.Kaplansky.ProperlyInfinite, OAI.Kaplansky.ActualAlgebra, OAI.Kaplansky.ContinuousOrthonormalStageFrame, OAI.Kaplansky.retainedLineStage, OAI.Kaplansky.testRank, OAI.Kaplansky.SmoothTestBase, OAI.Kaplansky.testProjectiveDimension
theorem OAI.Kaplansky.retainedGrouped_complementBundle_rank_lt line 65

theorem OAI.Kaplansky.properlyInfinite_retained_bundle_split line 84

Source documentation

From a proper-infiniteness witness in the actual matrix algebra, construct the ordinary complement vector bundle and the actual global bundle splitting. No characteristic-class hypothesis, bundle realization or norm bound is input.

theorem properlyInfinite_retained_bundle_split {m : ℕ} (hm : 0<m)
    (hpi : ProperlyInfinite (CStarMatrix (Fin m) (Fin m) ActualAlgebra)) :
    ∃ (R : ℕ) (_ : 0<R)
      (f : ContinuousOrthonormalStageFrame (retainedGroupedStage m R) (2*m*testRank m R 0))
      (H : f.ComplementSplitTotal ≃ₜ
        TotalSpace (retainedGroupedStage m R).Model (retainedGroupedStage m R).Fiber),
      (∀ z, (H z).proj=z.1.proj) ∧
      (∀ y : SmoothTestBase m R, Module.finrank ℂ (f.ComplementFiber y) <
        ∑ i : Fin R, testProjectiveDimension m R i) := by
…

Mentions: OAI.Kaplansky.ProperlyInfinite, OAI.Kaplansky.ActualAlgebra, OAI.Kaplansky.ContinuousOrthonormalStageFrame, OAI.Kaplansky.retainedGroupedStage, OAI.Kaplansky.testRank, OAI.Kaplansky.SmoothTestBase, OAI.Kaplansky.testProjectiveDimension