Science / reconstruction satellite for the Quantyra Jenny Connes rigidity audit.
Hypothesis failure for Ioana's Theorem 8.2 under a twisted comultiplication, Daniel Eric Fredriksen.
- Revised PDF · TeX
- Long-form report
- Source bundle · checklist · verification and Lean coverage
- Source identity and page anchors
This revision corrects our overstatement of Theorem 8.2's input and injectivity conclusion, addresses all three defenses in Nielsen's 49-page Section 21, and separately compares the hypotheses of the retained Section 9 appeal. The existing containment-to-intertwining obstruction remains bounded to this theorem application.
Release target: v0.1.3-report. Four independent role PASSes at 9aba11a, targeted public-verification-prose PASS at 896c1c9, and the root metadata/hash/scope PASS for that successor are recorded in the verification record. Final status-only carryforward requires root inspection and exact commit/body authorization before delivery. This is the prepublication gate record; delivery is recorded by the release. New version DOI: pending. Production of this version is authorized; arXiv submission and outreach require separate human approval. Historical approval does not approve these bytes.
Previous public science version: v0.1.2-report, DOI 10.5281/zenodo.21859653. Science concept DOI.
Lean: v0.1.1-obstruction, SHA c1e6dfb7347261336714e57de86e6f25c7627461, version DOI. The concrete Nielsen image situation is classically imported; containment-to-intertwining and hypothesis failure are proved on a semantic interface. An independently accepted fresh build of ConnesRigidity.NielsenThetaImage and twelve-declaration kernel audit are recorded in the verification record. This is a targeted build; the classical-import and partial semantic coverage limits remain unchanged.
This report does not decide Connes rigidity or the validity of OpenAI/Zhou counterexamples. Non-licensing of output by this application does not assert nonexistence of group morphisms or impossibility of other routes.
Canonical repositories: science, Lean. Theorem development belongs in the Lean satellite; this revision introduces no new theorem or Lean code.