test(computability): prove pair-first parsing prefix - #82
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 92ed44bdb2
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| The source input alphabet is only equivalent to `Bool`, so canonical pair bits | ||
| must first be transported through that equivalence. This phase proves the exact | ||
| trace that decodes duplicated first-component bits through the `01` delimiter. |
There was a problem hiding this comment.
This new public parser module proves and composes Mathlib StateTransition.EvalsToInTime certificates, but the module documentation only describes the parsing trace and does not cite the borrowed bounded-evaluation relation/transitivity API with authors, version, and precise declaration. That leaves later proof layers without the required provenance for the Mathlib clock machinery and its step-bound convention.
Useful? React with 👍 / 👎.
1 participant
What does this change?
Builds recursive bounded evaluations for decoding every bit of the canonical first component and reaching witness clearing. Small helpers package one-step traces and weaken execution bounds without changing the certified run.
This proves the parser prefix constructively rather than appealing to an informal decoder. This is stack layer 6 of 8.
How was it tested?
lake build --wfailpasseslake lintpassessorryor new axioms, or this PR does not change Lean proofs