OAI/Analysis/Kaplansky/Main.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Existence of a normalized two-quasitrace on the actual M48 algebra and a fixed positive contraction pair with universal real defect at least 1/144.

  1. theorem OAI.Kaplansky.actual_normalizedTwoQuasitrace_exists line 13
  2. theorem OAI.Kaplansky.kaplansky_quasitrace_counterexample line 17

    Distinct definitions of this name: ComparatorChallenges/KaplanskyQuasitrace.lean:48 (same statement text; different proof or body). Qualify references as OAI.Kaplansky.kaplansky_quasitrace_counterexample@path.