Hello! I've built a self-contained executable layer for the Bootstrapping stack on a fork branch (executable-proof-checking, and would like to offer it upstream.
Why, honestly: my project (lean-algorithmic-learning-theory) consumes Foundation's incompleteness results and needed a proof-decider that is at once executable and provably sound-and-complete. Until now I could only compose your provability predicate classically. This branch closes that gap on my side. The machinery seemed worth offering rather than keeping in a fork.
What it is, at V := ℕ: reducible substrate twins for the HFS primitives (core's Nat.sqrt/Nat.unpair don't kernel-reduce), executable mirrors of the syntax predicates and functions with proved agreement against your definitions, Theory.DecidableΔ₁ recognizers with 𝗣𝗔⁻'s axioms enumerated, and a kernel-decidable derivation checker with the bridge
provable_of_check : Proof.check L T d (encode σ) = true → T ⊢ σ
via your provable_iff_provable witnessed by in-file decide probes, positive and negative. It also includes both Primcodable instances from #506 in one self-contained file, through a uniform Primrec₂ interface (per-arity turns out provably insufficient ofNat reads the arity out of the code it decodes).
The bar throughout: machine-checked, warning-clean in every new and touched file, no maxHeartbeats; nothing existing depends on the new files, and the three touches to existing files each carry their reason in the commit. One honest boundary: checking a supplied witness runs, but exhibiting one at arithmetic scale is blocked by the encoding's magnitudes ({φ} = 2^φ) (a property of the Ackermann encoding, which earns its cost elsewhere). Nothing here asks to change it.
I'd open this as a single PR unless you'd rather have it sliced (natural cut points exist: substrate / mirrors + recognizers / checker + bridge / the #506 pair). Anything currently in flight I should rebase around?
Developed with heavy AI assistance (Claude Code), every result machine-checked and axiom-audited (provable_of_check depends on [propext, Classical.choice, Quot.sound], no sorryAx).
Closes #506. Related: #243, #757.
Hello! I've built a self-contained executable layer for the Bootstrapping stack on a fork branch (
executable-proof-checking, and would like to offer it upstream.Why, honestly: my project (lean-algorithmic-learning-theory) consumes Foundation's incompleteness results and needed a proof-decider that is at once executable and provably sound-and-complete. Until now I could only compose your provability predicate classically. This branch closes that gap on my side. The machinery seemed worth offering rather than keeping in a fork.
What it is, at
V := ℕ: reducible substrate twins for the HFS primitives (core'sNat.sqrt/Nat.unpairdon't kernel-reduce), executable mirrors of the syntax predicates and functions with proved agreement against your definitions,Theory.DecidableΔ₁recognizers with𝗣𝗔⁻'s axioms enumerated, and a kernel-decidable derivation checker with the bridgeprovable_of_check : Proof.check L T d (encode σ) = true → T ⊢ σvia your
provable_iff_provablewitnessed by in-filedecideprobes, positive and negative. It also includes bothPrimcodableinstances from #506 in one self-contained file, through a uniformPrimrec₂interface (per-arity turns out provably insufficientofNatreads the arity out of the code it decodes).The bar throughout: machine-checked, warning-clean in every new and touched file, no
maxHeartbeats; nothing existing depends on the new files, and the three touches to existing files each carry their reason in the commit. One honest boundary: checking a supplied witness runs, but exhibiting one at arithmetic scale is blocked by the encoding's magnitudes ({φ} = 2^φ) (a property of the Ackermann encoding, which earns its cost elsewhere). Nothing here asks to change it.I'd open this as a single PR unless you'd rather have it sliced (natural cut points exist: substrate / mirrors + recognizers / checker + bridge / the #506 pair). Anything currently in flight I should rebase around?
Developed with heavy AI assistance (Claude Code), every result machine-checked and axiom-audited (
provable_of_checkdepends on[propext, Classical.choice, Quot.sound], nosorryAx).Closes #506. Related: #243, #757.