OAI/Analysis/Naimark/Tracial.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NaimarkZFC.TracialStage.exists_supported_peak_pair_unconditional line 22
2. theorem OAI.NaimarkZFC.TracialStage.exists_joining_successor_unconditional line 46
3. lemma OAI.NaimarkZFC.ChronologicalStage.exists_supported_pair_unconditional line 70
4. theorem OAI.NaimarkZFC.ChronologicalStage.exists_joining_successor_unconditional line 89
5. def OAI.NaimarkZFC.ChronologicalStage.joiningChoice_unconditional line 114
6. lemma OAI.NaimarkZFC.ChronologicalStage.joiningChoice_height_unconditional line 119
7. lemma OAI.NaimarkZFC.ChronologicalStage.joiningChoice_treated_unconditional line 123
8. def OAI.NaimarkZFC.ChronologicalStage.scheduledRule_unconditional line 134
9. lemma OAI.NaimarkZFC.ChronologicalStage.scheduledRule_height_unconditional line 139
10. lemma OAI.NaimarkZFC.ChronologicalStage.scheduledRule_treated_unconditional line 153
11. theorem OAI.NaimarkZFC.ChronologicalStage.recursiveTower_treated_unconditional line 171
12. abbrev OAI.NaimarkZFC.ChronologicalStage.FullRule_unconditional line 183
13. abbrev OAI.NaimarkZFC.ChronologicalStage.fullTower_unconditional line 188
14. lemma OAI.NaimarkZFC.ChronologicalStage.fullTower_height_unconditional line 196
15. lemma OAI.NaimarkZFC.ChronologicalStage.fullTower_count_unconditional line 202
16. theorem OAI.NaimarkZFC.ChronologicalStage.fullTower_pure_reference_unconditional line 206
17. theorem OAI.NaimarkZFC.main line 243

    Distinct definitions of this name: ComparatorChallenges/Naimark.lean:44 (same statement text; different proof or body). Qualify references as OAI.NaimarkZFC.main@path.