·
1 commit
to main
since this release
Bounded claim
Nielsen definitional Θ package and by-construction bad-leg containment are imported as one classical semantic situation. Lean proves Ioana 8.2 hyp (2) fails, so rigid output is not licensed by that application.
Hardening vs v0.1.0
- Removed custom Popa bridge axiom
- Paper-strength exports in NielsenThetaImage
- SHA c1e6dfb
Not claimed
Connes T/F; OpenAI/Zhou CE; full Ioana; Lean construction of AG⊗L(H).
Companion report: Quantyra/connes-rigidity v0.1.1-report