Lean 4 audit core for Quantyra Jenny / Connes rigidity controversy.
Organization: Quantyra Inc.
GitHub: https://github.com/Quantyra/connes-rigidity-lean
Planning: https://github.com/Quantyra/Quantyra-Jenny-Planning (private) · local Quantyra-Jenny-Planning
Science sibling: https://github.com/Quantyra/connes-rigidity
License: Apache-2.0
Mathlib has only a thin von Neumann algebra skeleton (WStarAlgebra / double commutant). It does not yet contain group factors (L(\Gamma)), Bernoulli crossed products, Popa deformation/rigidity, or Ioana’s theorem. Therefore this package cannot fully prove or refute Connes rigidity today.
Ioana formalization foundations started; no Ioana theorem claimed. The current
foundation consists only of a mathlib double-commutant smoke test, a semantic ICC
definition, the Bernoulli shift action with its product probability measure and
measure-preservation proof, semantic almost-normal subgroup foundations, a
parametric semantic chosen faithful normal tracial-state record with its GNS L2 core,
and projection corners with support projection p as their multiplicative unit. In a
C*-algebra, these corners are norm closed and complete, inherit a non-unital
C*-algebra structure, and carry the supported unital C*-algebra structure whose unit
is p. Their canonical inclusion into the ambient algebra is explicitly non-unital.
For a nonzero support projection, the ambient trace restricts and normalizes to a
faithful tracial positive functional on this supported C*-corner. Generic rectangular
linear corners and supported partial-isometry identities are also available, without
installing an algebra structure on rectangular corners or asserting existence of a
nonzero partial isometry. Supported intersections with norm-closed non-unital star
subalgebras are also available as norm-closed C*-carriers. An optional project-local
predicate records directed-LUB preservation on positive sets for non-unital star
algebra homomorphisms; it is not imposed on any Ioana homomorphism. A separate transparent
semantic bundle can record a closed carrier and local projection-unit together with
explicitly supplied W*-structure on its supported corner and explicitly supplied
positive-directed-LUB preservation by its ambient inclusion. The W*-structure remains
explicit semantic data: no inhabitant or constructor deriving it from the other fields
is provided, and consumers install it locally. A transparent conditional-data structure
records the projections, plain non-unital star homomorphism, nonzero rectangular-corner
partial isometry, and ambient intertwining equation appearing in condition (1) of Ioana
Theorem 1.3.1. It asserts neither existence nor equivalence with another condition and
adds no unitality, normality, faithfulness, or exact support requirement. This remains
only a bounded norm-topological foundation. Carrier containment supplies a proved
condition-(1) witness using the nonzero local unit, so the Popa
containment-to-intertwiner bridge remains proved rather than axiomatized. One
classical fact is imported from Nielsen's NIEWTC definitional package:
Θ(f u_g) = f u_g ⊗ Φ(u_g) yields by construction a semantic image situation with
imageAlgebra ≤ rightBadLeg. From that fact, Lean proves that Ioana 8.2 hypothesis
(2) fails and that rigid output is not licensed by that application. The
imageAlgebra, the spatial W* tensor-product leg
A_G ⊗̄ L(H), and the W*-closure of the range are not constructed here from the
concrete opaque nielsenTheta. Opaque NI labels are not automatically identified
with, or discharged by, this semantic relation and require explicit iff or implication
premises.
No full Ioana theorem or Connes-rigidity result follows. No operator-topological W*-closure is provided. No concrete
finite von Neumann algebra witness, stronger inclusion continuity, or amplification
is provided. Conditional-expectation data can be supplied as a completely positive map from a
support corner onto the supported algebra, together with fixing, bimodularity,
trace-preservation, and explicit positive-directed Scott-continuity fields. This
types the finite double-sum proposition in condition (2), but supplies no
expectation inhabitant and proves no relation to condition (1). No Popa intertwining
or Ioana paper theorem is formalized.
What it does own (sorry-free; the semantic containment bridge is proved):
| ID | Content | Module |
|---|---|---|
| M1 | Connes ↔ ¬∃ counterexample | MetaLogic |
| M2 | Pair reductio ⇒ local ¬ L-iso schema | MetaLogic |
| T1 | Supplied semantic Nielsen image containment ⇒ ¬ Ioana 8.2 hyp (2) | NielsenThetaBlock |
| T2 | If rigid output ⇔ hyp2, Nielsen Θ yields no rigid output | NielsenThetaBlock |
| T3 | Imported Nielsen by-construction image situation ⇒ hyp (2) fails | NielsenThetaImage |
| T4 | Imported Nielsen situation ⇒ rigid output is not licensed by that hyp-(2) application | NielsenThetaImage |
| M3 | Nielsen claim / opaque NI interface link | MetaLogic |
| M5 | Conditional Nielsen pair skeleton | NielsenReductio |
| M6 | S006 status noGo |
S006Status |
See INTEGRITY.md.
lake build
bash scripts/check_no_sorry.sh
bash scripts/check_axiom_register.shCI (GitHub Actions): lake build + no sorry/admit + axiom/opaque register check on every push/PR to main.
- Tag:
v0.1.1-obstruction - Report: https://github.com/Quantyra/connes-rigidity/blob/main/docs/reports/2026-08-08-nielsen-ioana-theta-reductio-refutation.md
- Metadata: .zenodo.json, CITATION.cff
- Zenodo version DOI (v0.1.1): 10.5281/zenodo.21859309
- Zenodo concept DOI (all versions): 10.5281/zenodo.21845588
- Historical v0.1.0 version DOI: 10.5281/zenodo.21845589
Nielsen's definitional Θ package and by-construction bad-leg containment are imported as one classical semantic situation. Lean proves from it that Ioana 8.2 hyp (2) fails, so rigid output is not licensed by that application. Construction of the image algebra from concrete opaque Θ is not claimed. Constructing the spatial W* tensor product, crossed products, and the W*-closed range remains a Soft Blocker; the paper-oriented package does not fake those objects. Not claimed: Connes true/false; OpenAI/Zhou CE validity.
Do not cite this repo as proving Connes true/false or as settling OpenAI vs Nielsen. Chat critiques are not Lean theorems here.
- S002 satellites · S005 source pin · S006 Ioana/Θ audit · S007 reconstruction