| name | stage-journal-unit |
| description | Stage a result from THIS repo into the Noumenal Verified ML Journal. Use when a contributor wants to submit, stage, or publish a Lean result (a theorem + optional executable witness) to the journal / the Noumenal site, or asks "how do I add my repo / my theorem to Noumenal", "stage this for the journal", "make a noumenal.json", or "submit this unit". Produces a verified noumenal.json (schema unit.v2) and opts the repo in. Honesty-enforcing: it derives the tier and the trust base from the real artifacts and refuses to stamp an unproven result as accepted. |
Stage a journal unit
You are helping a contributor stage a result into the Verified ML Journal. The citable atom is
a (statement, proof, witness) triple. A unit is ACCEPTED only when three independent checks
pass together: PROOF (the kernel checks the proof), FAITHFULNESS (a human-certified gloss
says the theorem means what the prose claims), and WITNESS (the executed value lands inside a
kernel-certified interval). Tier (T0/T1/T2) is derived from what is actually true, never
declared. The schema is unit.v2.json.
Two rules that govern everything you do here:
- Never inflate. You report what the artifacts prove, not what the author hopes. A hidden
sorry is staged as an open ChallengeCrown, not as an accepted unit. The tier you write is the
tier the checks earn.
- Name the base. Every leg is "verified modulo a named base": the Lean kernel, the axioms it
actually uses (
#print_axioms), the pinned Mathlib, and any FFI/oracle boundaries. You enumerate
it; you do not hide it.
Substrate exception (important). The proof leg and the witness leg are INDEPENDENT. Each has its
own dependency closure and its own named base. Do not force the experiment onto the same
substrate as the theory, and do not write a shared-substrate link between them. A contributor may
bring a theory verified on their Lean and an experiment certified in their own sandbox.
The sequence
Work through these steps with the contributor. Run real commands; do not guess outputs.
1. Discover the unit
Find the candidate in the repo: the Lean module, the headline declaration (the statement + its
proof term), and any executable witness (an interval-membership theorem + the binding that runs
it). If the declaration's body is sorry, this is an open ChallengeCrown — stage it as such
(sorry_free: false, no tier), not as accepted. Ask the contributor which declaration is the unit
if it is ambiguous.
2. Run the PROOF check (kernel) and derive the base
- Build the module:
lake build (or lake env lean <file>). It must succeed with no sorry.
- Audit axioms on the exact declaration:
#print_axioms <decl> (via lake env lean on a tiny
script, or read it from the build). Record the axiom list as proof.axiom_manifest.
- Record
proof.base: kernel (the Lean version from lean-toolchain), axioms (the whitelist
actually used), mathlib (the pinned commit/toolchain), and any ffi boundaries.
- If the only axioms are
propext, Classical.choice, Quot.sound and there is no FFI, this is a
kernel-clean base. If more are present, list them — named, not hidden.
3. Run the WITNESS check (sandbox), if there is one
- If a witness exists: run it and confirm the executed value lands inside the interval the
interval_decl theorem certifies. "Match" means interval-membership, never bit-exact.
- Record
witness.kind (interval for the strong case; figure/empirical for softer evidence;
none if there is no witness), the binding, interval_decl, interval, sandbox, and the
witness's OWN base and closure (separate from the proof's).
4. Draft the FAITHFULNESS gloss
Write gloss.text: one short paragraph, standard vocabulary, saying what the theorem actually
means. Leave gloss.certified_by: null — the editor certifies it, the author only drafts. No gloss,
no DOI.
5. Derive the tier (do not let the author pick it)
- T0 = proof check passes (sorry-free, axiom-audited), no witness.
- T1 = T0 + a witness that runs (
witness.kind != none and it executed).
- T2 = T1 + the executed value lands in the certified interval on held-out inputs.
Set
checks to your local pre-check result; CI re-verifies authoritatively before ACCEPTED.
6. Emit noumenal.json and self-verify
- Build the manifest with
node skills/stage-journal-unit/lib/stage.mjs (it assembles the unit,
derives tier/checks.accepted, and validates against schemas/unit.v2.json).
- Place it at the repo root as
noumenal.json with "noumenal": true, "version": 2.
- Show the contributor the unit: its tier, its named base, what is still open. Confirm the prose is
standard vocabulary (no in-house jargon: URT, URS, KK/KU, "discovery tetrad", etc.).
7. Opt in
On the contributor's go-ahead, commit noumenal.json. The journal aggregator (cron + manual)
discovers any repo with noumenal: true, RE-RUNS the three checks authoritatively, pulls live proof
code for public repos, and renders the unit. CI is the gate; your local run is the honest draft.
If you are blocked
- No Lean toolchain locally: derive everything you can statically (statement, gloss, base from
lean-toolchain + lakefile), set checks.* : "pending", and let CI run the proof/witness. Say
plainly that the unit is unverified-pending, not accepted.
- The proof has a
sorry: stage it as an open ChallengeCrown (a bounty), honestly. That is content,
not a failure to hide.
- The witness does not land in the interval: the unit is T0 (or the interval/claim is wrong). Report
the gap; do not widen the interval to force a pass.
