[heathsanchez]

Objective

Expose a consequential distinction that a downstream observation cannot decide, while preserving independent reviewer provenance and source-dependent withdrawal. Advisory research integration, not a deployed universal code auditor.

Implementation

• projection-claim-v1: source-bound finite collision checker. Opposite independently admitted target verdicts under an identical observation form a bounded NAMED_OBSTRUCTION. Finite no-collision, missing proof policy and source changes remain UNKNOWN for universal sufficiency.
• Authenticated GitHub readback: optional claim enters Check → permitted Resolve proposals → Monitor source-change withdrawal, with MathGraph's own Check runs excluded as independent evidence.
• signed-projection-review-v1: Ed25519 review envelope signs the reviewer ID, exact authenticated PR subject, requirement, finite witness, and evidence receipt/digest; public-key trust roots come only from the separate trusted host. Forged, altered, stale or incomplete packets are UNKNOWN—even with green CI or no native checks. Raw trusted-host and signed routes are mutually exclusive.
• Historical frozen L4YAML parser/raw SOH regression and synthetic-only PR fixture; historical Lean proof cited but not rerun in this feature.
• Workflow now executes the finite quotient, signed review, projection, L4 witness and previous Check/Resolve/Monitor tests before read-only GitHub API observation.

Exact evidence (current 8 Nov 2026)

• Latest draft research head 3c7f79e2, tree a030fcb653554edef5a02bf446b3786d79f1076a (matches local source tree).
• GitHub Actions run #42465188680, job 128682954667: SUCCESS, including contract/signed-review regressions and live PR/Checks API readback.
• Local full JS tests: 649 total / 638 passed / 11 skipped / 0 failed. New exact-source handoff tests 3/3; targeted suite 21/21.
• Actual first-party artifact ID 13611685532, ZIP SHA-256 5319cf1cec5d9a1466995da87610b488fdab64560ec44b7c89e1c2f39c531e9b (matched GitHub metadata). Its native observation and intended requirement remain UNKNOWN, and it excludes self-check 128682954667.
• Source-qualified independent L4YAML review request: YAML 1.2.2 §5.1, exact bytes 2361 versus 2301, frozen L4 source 64795a8d, separate Lean proof commit b882e5b2, original Lean artifact SHA-256 f60e48bc…. The four independently reviewable tasks are explicitly PENDING and no signature was issued.
• Important fail-closed boundary: attempting to apply the historical L4 witness to the current MathGraph PR head returns UNKNOWN / WITNESS_NOT_BOUND_TO_CURRENT_PR_HEAD. No cross-repository admission is claimed.

Limits / non-goals

• The signature authenticates review of packet bytes; it does not replay a cited proof artifact, establish the reviewer's mathematical correctness, or ratify a human requirement. No actual external signed-review receipt was issued by this work.
• Existing default first-party runner and deployed hosted pilot do not inject the optional signed policy or keys. The pull_request workflow executes PR merge-ref code, so it is not a protected policy issuer.
• Generic requirement discovery, independent semantic verdict qualification, protected trust distribution, full L4YAML language fidelity, universal positive correctness and deployment remain UNKNOWN.
• No new Check Run publication, production deployment, or merge.

Review focus

1. Protected signer/key distribution separated from PR-authored code.
2. Exact statement/source/witness/receipt signature binding and UNKNOWN on all invalid or stale inputs.
3. No promotion from finite observations or review signature to unbounded semantic proof without independent replay.

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated
mathgraph	Ready	Preview	Nov 8, 2026 9:02am UTC