Skip to content

Witnessed Derivation Calculus

Choose a tag to compare

View all tags
@unpingable unpingable released this 27 Jun 05:54
· 139 commits to main since this release
v1.4.0
8854d53

Promotes the ratified Witnessed Derivation Calculus into the canonical public Lean
surface as LeanProofs.Witnessed.* — Mathlib-free, build-graph-isolated, and
footprint-gated in CI.

Additive minor release: the stable 1.x Admissibility Kernels surface is unchanged.
(Why 1.4.0 and not 2.0.0 — nothing in 1.x breaks; semver tracks the consumer surface,
not milestone size. 2.0 is reserved for a structural strengthening of the calculus.)

Added

  • Canonical LeanProofs.Witnessed.* namespace + aggregator; separate Mathlib-free Witnessed lib
  • Downstream consumer example (LeanProofs/Witnessed/Examples.lean)
  • Footprint regression gate (scripts/check-witnessed-footprint.sh) + CI wiring
  • Public frontier register (docs/WITNESSED-FRONTIER-REGISTER.md)

Not a revival of the retired maximal "Admissibility Calculus"; universal normalization,
non-suppression, full composition-classification, and model→world transfer remain
explicitly fenced. Full detail in CHANGELOG.md.

Assets 2
Loading