v0.1.1-obstruction: paper-strength Nielsen Ioana+Theta block

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

v0.1.0-obstruction: Nielsen Theta blocks Ioana 8.2 hyp (2)

Bounded Lean release

Main theorem: nielsenTheta_blocks_ioana82_hyp2 in ConnesRigidity.NielsenThetaBlock.

Nielsen's Θ(f u_g)=f u_g ⊗ Φ(u_g) cannot satisfy Ioana Theorem 8.2 hypothesis (2), because im(Θ) ⊆ A_G ⊗ L(H) by construction. The Ioana+Θ reductio therefore does not obtain rigid-case group morphisms from that application.

Bridge axiom: image_subseteq_M1_LH_negates_niRight (containment ⇒ ¬ niRight).

CI: lake build, no sorry/admit, axiom register.

Report: https://github.com/Quantyra/connes-rigidity/blob/main/docs/reports/2026-08-08-nielsen-ioana-theta-reductio-refutation.md

Non-claims

• Does not prove or refute Connes rigidity.
• Does not validate or refute OpenAI or Zhou counterexamples.
• Does not fully formalize Ioana (2011).