Repository navigation
NOESIS P-NP formal gap ledger v1 - #429
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: 6340a8c32e
ℹ️ 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".
| structure PolyTimeCertificate (chooseK : ChooseK) where | ||
| polynomial : ℕ → ℕ | ||
| polynomial_nonnegative : ∀ n, 0 ≤ polynomial n | ||
| bound : Prop |
There was a problem hiding this comment.
Because bound is stored as a Prop rather than as a proof of a concrete runtime bound, constructing PolyTimeCertificate does not prove any complexity claim: a caller can fill this field with True or even False and VerifiedChooseK will still treat the selector as complexity-certified. In contexts that rely on VerifiedChooseK to mean a machine-checked polynomial-time certificate, this makes the obligation vacuous; the field should instead encode and require proof of a defined cost-model bound for chooseK.
Useful? React with 👍 / 👎.
Purpose
Add the first explicit epistemic gap ledger for the NOESIS/P-NP oracle track.
What this records
NOESIS/Oracle.lean.chooseKobligation that remains open.src/ramsey_haar_oracle.py.src/pnp_oracle_bridge.py.Epistemic rule
This PR does not assert P = NP. It makes the missing proof obligations machine-auditable and prevents a declared
O(1)metadata field from being promoted to a theorem without a complexity certificate.Next milestone
Construct and formally verify a concrete deterministic
chooseK, then prove its complexity under an explicit input representation/cost model.