pub const PRELUDE_VERSION: &str = "logos-coc-6";Expand description
The prelude/axiom-set version a certificate was produced against. A re-checker may refuse certificates minted against an axiom set it does not recognise. Bump this whenever the trusted prelude changes.
logos-coc-6 DEFINES Quot_rec. The dependent quotient eliminator is a checked
definition — Quot_lift into Lean’s PSigma, Quot_ind, and a transport — so it
leaves the trusted base, and its axiom closure is Quot_sound, read through its
body. Quot_lift’s target is Sort v, as Lean’s is, which that definition needs.
Quot, Quot_mk, Quot_lift and Quot_ind keep the registered primitive
identities tied to their computation rules and are not reported as assumption
leaves while that identity is live. Quot_sound, propext, Classical_choice
and the opaque Float operation surface remain assumptions.
Earlier tags, including logos-coc-5, are refused even when a particular
proof would still check: a certificate claims to have been checked against
its stated assumptions, and no validated migration rewrites that claim.
The wire schemas and entry encodings are unchanged; only the trusted prelude
version changes with its primitive computation and assumption accounting.