v1.1.0 — corrected & honest (depth-22 theorem + conjecture, Lean-verified, AI-disclosed)

Major correction-and-honesty release superseding v1.0.0. Same concept DOI (10.5281/zenodo.20370090) now resolves here.

What changed since v1.0.0

v1.0.0 over-claimed an all-depths universality proof. This release states only what is established and labels the rest honestly.

• Universality: now a theorem 'established through depth 22' (machine-certified in Lean 4, symbolically over Q(a,b)), plus an explicit all-depths Conjecture with a stated candidate obstruction (the rotation-number zeta_T = (a+bi)/(a-bi) has a shape-dependent minimal polynomial). The earlier 'Phi_T injective' proof step was false and has been removed.
• Class C faithfulness (distinct legs, all n>=3): proof repaired — angle-irrationality (Niven-Conway-Jones) reducing to rank-0 descent on the Cremona curves 24a1, 32a2, 72a2 (32a2 was mislabeled 'E_6' in v1.0.0). Tits' theorem applied only after the Coxeter matrix is established. Sage scripts in code/mordell/ certify finiteness via rank 0.
• Closed-form r_n = 1 + 2cos(2pi/(n+3)): derivation corrected (the earlier diagram paragraph was internally inconsistent); derived from Steinberg's formula.
• Lean 4 formalization (lean/): eight length-10 relations and Schur steps as kernel-checked ring proofs; depth-22 universality certificate via native_decide; cyclic-ideal equality verified to N<=16 (code/ideal/).
• beta_2: the unsupported '1.4718' replaced by the honest empirical value (~1.50, ~1.497 at depth 42; exact value open).
• AI-use acknowledgment added (the work is AI-led under human direction).
• Related work (Sadun, Frettloh) added; prose neutralized.

Honest status

• Proven: universality through depth 22; the eight length-10 relations over Q(a,b); closed-form r_n; Class C faithfulness in every dimension; the Schur determinant identity.
• Open: all-depths universality (conjecture, with a known candidate obstruction); the exact asymptotic ratio beta_2.

Contents: paper/ (main + companion PDFs/TeX), paper/OEIS/ (submission drafts + b-files), code/ (Rust BFS, SymPy/Sage verifications, Mordell + ideal scripts), lean/ (two Lean 4 projects), reproduce/.