Predecessor: v1.3 candidate, RATIFIED at df9e7b7 (RATIFICATION-v1.3.md).
Status of this doc: candidate definition-of-done. Non-binding until the operator opens the slice.
2.0 is NOT “more theorems.” The mathematical gate is already cleared (v1.3, ratified). 2.0 is the public-contract promotion. Clean exit criterion:
The Witnessed Derivation Calculus moves from a ratified experiment to the supported public surface, with a tested migration path and at least one non-experimental consumer.
The remaining work is packaging, not discovery. No new mathematics unless migration exposes a genuine hole.
Public module surface. Successor stops living only under experiments/. Canonical modules
land under the supported LeanProofs/Admissibility namespace (or its deliberate successor), the
public aggregator imports them, and they build in the default target — not only via
lake build Successor.
Stable contract. Freeze names and boundaries (no further terminology churn without
deprecation) for: the witnessed-derivation judgment; paid composition / cut; revocation
non-manufacture; normalization (explicitly scoped to the canonical freshness embedding);
WitnessedDiscipline as a model filter beside the calculus; the four discipline axes;
Discriminating retired/factored through SemanticNontrivial.
Migration from 1.2. Exact old→new import and theorem-name map; compatibility shims where cheap and honest; explicit removals where compatibility would preserve the wrong abstraction. A public 1.2 user can tell whether they must change anything without reading repository archaeology.
experiments/no_free_lift_wiring/
uses the supported API and compiles in CI. Two grades, either satisfies 2.0 — but the completion
record must say which, because an external consumer is stronger evidence:
agent_gov correspondence does NOT satisfy this gate — AG is operational evidence, not a Lean dependency or verified implementation.
Release verification. Default build green; public examples green; no live sorry/admit;
recorded axiom footprints still within the ratified ceiling (≤ [propext, Quot.sound]); clean
public import graph; no accidental dependency on playground/quarry/scratch branches; release
built from a clean checkout, not merely the current warm worktree.
Public claim alignment. README, CHANGELOG, module headers, migration note, and ratification record must all agree that: the name is Witnessed Derivation Calculus; it is a narrow calculus of witnessed movement, not a maximal unifying kernel; normalization is model-scoped; the discipline is adjacent, not constitutive; agent_gov is an implemented/convergent external instance, not a verified reduction; refusal legibility remains future work.
Operator promotion. The operator explicitly accepts the supported API and migration cost, then:
removes candidate language; sets version 2.0.0; tags and releases; retires or redirects the old
public aggregator/shim per the migration decision.
The final promotion record must cite the verification commit/receipt (gate 5) and mark each of gates 1–6 explicitly PASS — not a bare “operator accepts” checkbox. Sign-off cites evidence, or it is just another robe.
These are later work or separate projects.
df9e7b7).The 1.3 package + ratification are committed. Next: open a deliberately boring 2.0 public-surface migration slice — gates 1–7 above, no new mathematics unless migration exposes a genuine hole. The artifact now has to survive packaging.