Conversation
`Completeness.lean` holds 250 hand-transcribed models, one per spec,
each with a theorem asserting the module is Icarus-lowerable. 114 of
them have `functions := []`, and 104 of those have an empty `Env` too. A
theorem about an empty module says nothing about its spec:
`native_decide` on an empty structure proves something true and useless.
`max_vacuous`, the ratchet that exists to stop that number growing,
counts 44 -- because it reads the mismatch ledger, and an entry only
reaches that ledger if the model ALSO disagrees with the Rust
classifier. Whether a theorem is vacuous has nothing to do with whether
the classifier happens to disagree.
models in the file 250
with `functions := []` 114
...and an empty Env too 104
counted by max_vacuous 44
vacuous and INVISIBLE to it 70
A ratchet measuring a subset of its own subject is worse than no
ratchet, because the number it reports looks like the number you care
about. Its 44 marks are all correct -- zero entries marked
`model_empty` that are not -- so this is a coverage gap, not a wrong
reading.
Measured twice, by a throwaway Python scan and by the shipped Rust, and
the two agree on every one of the five numbers.
The command refuses rather than printing zero when it matches no
modules: a zero from a scanner that found nothing is indistinguishable
from a clean file, and the file's shape is exactly what would change
under it.
4 tests.
WHAT THIS IS NOT. Last pass I named "write real Lean models for those
four" as the only honest way to lower `max_vacuous`, and I am not doing
it. `lean`, `lake` and `elan` are not installed here. A faithful model
may make its theorem FALSE -- the classifier says `Rust=false` for those
specs -- which is the correct outcome and not a bug, but I cannot tell
the correct outcome from a transcription error without building it.
Writing a proof I cannot check and pushing it to see what CI says is the
thing this repository exists to prevent.
Refs #2747
gHashTag
enabled auto-merge (squash)
August 29, 2026 21:33
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-29 21:34:06 UTC
Summary
Seal Status
|
Contributor
PR DashboardGenerated at: 2026-08-29 21:35:06 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
This was referenced Aug 29, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Completeness.leanholds 250 hand-transcribed models, one per spec, each with a theorem asserting the module is Icarus-lowerable.functions := []Envtoomax_vacuousA theorem about an empty module says nothing about its spec:
native_decideon an empty structure proves something true and useless.max_vacuous— the ratchet that exists to stop that number growing — reads the mismatch ledger, and an entry only reaches that ledger if the model also disagrees with the Rust classifier. Whether a theorem is vacuous has nothing to do with whether the classifier happens to disagree.A ratchet measuring a subset of its own subject is worse than no ratchet, because the number it reports looks like the number you care about. Its 44 marks are all correct — zero entries marked
model_emptythat are not — so this is a coverage gap, not a wrong reading.Measured twice, by a throwaway Python scan and by the shipped Rust, agreeing on every one of the five numbers.
The command refuses rather than printing zero when it matches no modules: a zero from a scanner that found nothing is indistinguishable from a clean file, and the file's shape is exactly what would change under it. 4 tests.
What this is not
Last pass I named "write real Lean models for those four" as the only honest way to lower
max_vacuous. I am not doing it, and the reason is not effort.lean,lakeandelanare not installed here..github/workflows/lean-proofs.ymlhas alake build, so the instrument exists — just not where I am. And a faithful model may make its theorem false: the classifier saysRust=falsefor those four specs, so an honest transcription might be unprovable. That would be the correct outcome rather than a bug — but I cannot tell the correct outcome from my own transcription error without building it.Writing a proof I cannot check and pushing it to see what CI says is the thing this repository exists to prevent. The count is reported instead.
Refs #2747