lean

2.0 Release Gate Receipt — Witnessed Derivation Calculus

Predecessor: v1.3 candidate, RATIFIED at df9e7b7 (RATIFICATION-v1.3.md). Status of this doc: PASSED / historical release receipt. v2.0.0 is tagged with peeled target b4bd02b (2026-06-29).

What this gate was — and what shipped

This file began as the public-contract promotion gate: move the Witnessed Derivation Calculus from ratified experiment to supported public surface, with a tested migration path and at least one non-experimental consumer. That packaging gate shipped in 1.4.0. It governed a compatibility-surface release, not permission to state or prove the calculus; it is not a current downstream-consumer prerequisite for formal work.

v2.0.0 then used the reserved WDC integer for the structural strengthening that the frontier register required: model-independent admitting-class normalization (normal_form_iff_of_commutes) plus a necessity counterexample (commutes_is_necessary), with the audit fence hardened around the release. Existing 1.x imports remain additive/non-breaking; the integer marks the structural milestone, not API churn.

Completion record

• Release tag: v2.0.0
• Tag target: b4bd02b
• Gate 1 — Public module surface: PASS (LeanProofs.Witnessed.*, default target)
• Gate 2 — Stable contract: PASS (frozen WDC names carried forward; 2.0 theorem additive)
• Gate 3 — Migration from 1.2/1.4: PASS (MIGRATION-NOTES.md, README/CHANGELOG alignment)
• Gate 4 — Non-experimental consumer: PASS in-repo (LeanProofs/Witnessed/Examples.lean); stronger downstream fixture added at downstream/wdc-v2-consumer/
• Gate 5 — Release verification: PASS at release prep (default build, WDC footprint, axiom/native_decide/mathlib gates)
• Gate 6 — Public claim alignment: PASS after post-release cleanup of stale candidate wording
• Gate 7 — Operator promotion: PASS (version set to 2.0.0, tagged, released)

Required gates

1. 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.

2. Stable contract. Freeze names and boundaries (no further terminology churn without deprecation) for: the witnessed-derivation judgment; paid composition / cut; revocation non-manufacture; normalization (freshness instance in 1.4.0; model-independent admitting-class theorem in 2.0.0); WitnessedDiscipline as a model filter beside the calculus; the four discipline axes; Discriminating retired/factored through SemanticNontrivial.

3. 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.

4. Non-experimental consumer. At least one consumer outside 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:
   • public in-repo consumer — a public examples module or another canonical Lean module in this repo;
   • external downstream consumer (stronger) — a small separate Lean project pinned to the release.

   agent_gov correspondence does NOT satisfy this gate — AG is operational evidence, not a Lean dependency or verified implementation.

5. 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.

6. 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 an admitting-class theorem, not universal normalization; the discipline is adjacent, not constitutive; agent_gov is an implemented/convergent external instance, not a verified reduction; refusal legibility remains future work.

7. 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.

NOT required for 2.0 (do not hold the release hostage)

• Rust agent_gov; AG formally importing or verifying Lean.
• A universal normalization theorem.
• The refusal-legibility / continuation-bearing-refusal theorem.
• P4.
• A grand maximal-calculus synthesis.
• Every scratch theorem finding a respectable home.

These are later work or separate projects.

Current state

• Formal artifact: done.
• Ratification: done (df9e7b7 for v1.3; v2.0.0 at peeled target b4bd02b for the structural release).
• 2.0 blockers: none remaining in this repository. Post-release wording cleanup and the downstream fixture are documentation/receipt hardening, not release blockers.

Next honest route

Keep 2.0 closed. Future work should open a new named slice instead of reusing this gate: reachability-based composition classification, cut-elimination, non-suppression, or witnessed clocks each needs its own distinct formal statement, overlap review, and receipt. None waits on a downstream consumer.

This site is open source. Improve this page.