[heathsanchez]

Scope (first-party only)

Adds a single, isolated issue_comment: created listener for the exact comment @MathGraph /check by owner GitHub ID 32909488 on first-party PR #239. No generic community intake, model calls, automatic repairs, or untrusted PR code.

• The three jobs check out immutable, qualified OMM implementation SHA 079f0a6c7802f2a4482c9e3778e801a6880c86dd (from draft feat(check): bounded OMM Lean claim-audit bridge (no L4YAML changes) #270), never the commented PR's head.
• Admission re-reads the real GitHub comment and exact PR239 head/source; edited/foreign/stale events are refused.
• The pinned Lean 4.28.0 / Mathlib replay runs in a separate credentialless job and emits bounded native receipts.
• The registered App token exists only in a separate publishing job that requalifies the event, source and native artifacts, writes one neutral check with an isolated OMM /check identity, and verifies the published App identity and exact head.
• The previous push-triggered -claim record and generic -check/-fix demo are untouched.
• This PR contains only .github/workflows/check-omm-owned-slash.yml. No Workers, /pilot, examples or L4YAML files are modified.

Evidence

Local test-driven qualification: 72/72 OMM + listener safety tests, zero failures. The pinned implementation was staged on draft #270 without merging that feature branch; CI passed on the exact code head.

Limits

Live issue_comment→native→App readback remains UNKNOWN until a fresh first-party /check comment is posted and that run's artifacts and published Check are verified. This workflow is deliberately owner/PR-specific, not a community verification service or mathematical-intent warrant.

[vercel]

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

Project	Deployment	Actions	Updated
mathgraph	Building	Preview	Nov 5, 2026 1:36am UTC