[timbrigham]

Brings main up to illustrated (through a8876d3): 378 non-merge commits, 329 files changed, +95,344 / -23,135 lines. main has no commits that illustrated lacks, so this is a fast-forward of content; nothing is reverted.

Licence change. On main the repository is under CC BY-NC-ND 4.0, with the fonts in scripts/fonts/ excepted. After this merge it is under two licences, as NOTICE sets out:

• Code: Apache License 2.0 (LICENSE). The .lean files, scripts/*.py, tools/**, .github/**, .claude/**, CLAUDE.md, lakefile.toml, lake-manifest.json, lean-toolchain, ssot.json, .zenodo.json and the other configuration files.
• Documents: CC BY-NC-ND 4.0 (LICENSE-DOCS). The PDFs at the repository root, every Markdown file except CLAUDE.md and those under tools/ and .claude/, and the site layouts in _layouts/.
• Third-party material is listed in NOTICE and keeps its own licence. This covers the vendored and ported Lean (ZeroParadox/Vendored/, ZeroParadox/Ordinal/NaturalOpsPow.lean), which stays under Apache 2.0 with its original copyright, and the fonts.

What it carries, by area:

• New Lean files.
  • ZeroParadox/Computability/KleeneChoiceFree.lean: Kleene's second recursion theorem for a transformation given as a code, kleene_cf, with the fixed point an explicit term. It is a fixed point up to eval, not a literal one, and the proof does not use Classical.choice.
  • ZeroParadox/Computability/UniversalChoiceFree.lean: a universal code for Mathlib's Nat.Partrec.Code whose correctness proof does not use Classical.choice, universal_code_cf (existential, built from a small-step machine), and a code that both prints itself and is universal, selfref_universal_exists_cf, stated with the choice-free predicates SelfPrintsCF and UniversalCF. Their equivalence with the Mathlib-phrased predicates (selfPrints_iff_cf, universal_iff_cf) uses Classical.choice.
  • ZeroParadox/Meta/AxiomLedger.lean: a ledger of declared axiom profiles. Elaboration fails if a recomputed profile differs from its row, or if a theorem of the two files above has no row. The check uses the vendored auditor in ZeroParadox/Vendored/CorpusAudit/ (from GuardianEngineAI/corpus) and runs in the new workflow .github/workflows/axiom_ledger.yml. A control file, AxiomLedgerControl.lean, plants one wrong profile, and the workflow fails unless that row and nothing else turns red.
  • ZeroParadox/Information/Disjunctive.lean: disjunctive sequences (tapes ℕ → Bool on which every finite word occurs). The all-false tape is not disjunctive, a primitive recursive disjunctive tape exists, the fair-coin tape is disjunctive almost surely, and no periodic tape is disjunctive. On a disjunctive tape every code word occurs; nothing is said about executing one.
  • ZeroParadox/Die.lean and ZeroParadox/DieCannotBe.lean: the record Motion (an idempotent partial self-map and a step relation) and an index of its premises with members and non-members. Every type carries a Motion, so the premises are stated as hypotheses and carry the content.
  • ZeroParadox/Category/DieNucleus.lean: on a meet-semilattice, a Motion whose map is total, raising and preserves ⊓ gives a Mathlib Nucleus. snapNucleus on Ordinal is a member; the notation carrier SynONote has no snap nucleus (no_snap_nucleus).
  • ZeroParadox/Category/LawvereTwoAdic.lean: on ℤ_[2] and on ℤ, add-one has no fixed point, so no class of self-maps containing it has a relativized Lawvere witness.
  • ZeroParadox/Category/IgnoranceSeam.lean: filling the unknown digits of a finite partial stream with false or with true sends the empty stream to the least or the greatest element of the pointwise order on ℕ → Bool. Complement carries prepend-false to prepend-true.
  • ZeroParadox/Settheory/GraphBisim.lean and ZeroParadox/Settheory/HypersetOrder.lean: finite membership graphs up to bisimulation. Taking the well-founded part preserves bisimilarity (wfPart_same) and dropping loops does not (dropLoops_not_same). Under the subset order, pruning is a kernel operator (pruneKernel).
  • 18 new companion .md files, 17 of them beside .lean files already on main and one beside Disjunctive.lean.
• Documents. 37 root PDFs are rebuilt, and ZP_Philosophical_Question.pdf and its build script are removed. Versions move in register.md. For example, ZP-E goes from 3.50 to 3.61, ZP-B from 1.18 to 1.30 and ZP-R from 1.6 to 1.20.
• Claims narrowed or corrected. Some examples:
  • ZP-C's T-BUF now says execution is conditional. Earlier text said unbounded surprisal forces it, but that step is the occurrence commitment, which DA-1 consumes and does not supply.
  • The note on c3_irreversible in ZeroParadox/Valuation/Padic.lean no longer calls 0 the unique point at the base of a nested clopen-ball stack, which holds for every point of ℚ_[2]. It now says topology does not single 0 out: 0 is the additive identity and the only point of valuation top, and whether that makes it least or greatest depends on the order chosen.
  • ZP-R drops the conjecture that Lawvere's theorem accounts for every face, which was measured false. In its place is one statement in Section III that treats the faces case by case.
  • ZP-P now limits quine_atom_unique to x = {x}.
• Tooling. 61 files under tools/ change, along with the command files under .claude/commands/ and .claude/settings.json.

Known open items: ordinary-severity imprecisions remain in the prose and are tracked. This merge fixes only what the range already contains.

No release is cut by this merge.