feat(computability): define pair-first wrapper - #78
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: 48fa77a186
ℹ️ 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".
| .pop (.source certificate.tm.k₀) (fun state symbol => { state with second := symbol }) | ||
| (.branch (isDuplicate certificate) | ||
| (.push .reverse (firstSymbol certificate) (resetAt certificate.tm .readFirst)) | ||
| (.branch (isDelimiter certificate) (resetAt certificate.tm .clearSecond) .halt)) |
There was a problem hiding this comment.
For an empty input stack, which is not a canonical Arora--Barak pair because even an empty first component needs the 01 delimiter, readFirstStatement pops none, readSecondStatement pops none, and this raw .halt runs with the initial state and all stacks empty. That is the wrapper's canonical haltList [], not a rejection/non-output, so the parser has a false malformed-input base case; add an explicit malformed state/flag or otherwise avoid a canonical halt on this path.
Useful? React with 👍 / 👎.
| This finite wrapper decodes the first component of the canonical Arora--Barak | ||
| pair, restores that bit string as the input of an arbitrary certified source | ||
| machine, and then simulates the source. The wrapper charges the complete pair, |
There was a problem hiding this comment.
This new module borrows the Arora--Barak pair convention but only names the authors; the repo requires title, year/version, and a precise section/page, so downstream proof provenance cannot distinguish this wrapper from other pairing conventions. Please add the same precise citation used by the binary-string pairing definition near this module text.
Useful? React with 👍 / 👎.
1 participant
What does this change?
Defines the finite two-stack-machine wrapper needed to evaluate a certified Boolean function on the first component of a canonical pair. The machine decodes the first component, consumes the complete second component, restores the source input, and embeds every source statement with source halt preserved exactly.
This is the concrete specialized composition machine required by the eventual
P ⊆ NPproof. It is stack layer 2 of 8 and depends oncodex/verifier-np-foundations.How was it tested?
lake build --wfailpasseslake lintpassessorryor new axioms, or this PR does not change Lean proofs