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).