Skip to content

feat(interval): pin PNT migration inventory - #9256

Merged
kim-em merged 1 commit into
mainfrom
agent/interval-pnt-inventory
Aug 14, 2026
Merged

feat(interval): pin PNT migration inventory#9256
kim-em merged 1 commit into
mainfrom
agent/interval-pnt-inventory

Conversation

@kim-em

@kim-em kim-em commented Aug 14, 2026

Copy link
Copy Markdown
Owner

Summary

  • pin the PNT+ source, LeanCert/Mathlib revisions, toolchain, and all tracked Lean-source content
  • inventory executable and textual interval tactics, direct imports, reviewed interface ownership, trust-residue sites, and generated Table 10/Table 12/FKS2 workloads
  • add an offline integrity gate plus maintainer refresh, source-verification, inspection, and evidence-classification workflows
  • record a concrete HexInterval migration acceptance corpus without promising LeanCert API compatibility

Audit surface

  • 280 executable interval_decide sites and 60 executable interval_auto sites
  • 16 direct LeanCert imports and six load-bearing interface families
  • 107 qualified reference occurrences retained as inventory-only evidence under reviewed interface provenance
  • 83 executable textual native_decide trust-audit candidates
  • Table 10: 87 target sites and 38 supporting a₂ sites
  • Table 12: 26 structurally parsed rows × five reviewed columns = 130 checks
  • FKS2: 13,590 cells across fourteen shards
  • 449 migration records intentionally remain pending; this PR establishes the audited backlog, not the migration claim

Verification

  • python3 -m unittest scripts.maintenance.test_pnt_inventory (23 tests)
  • offline pnt_inventory.py --check
  • exact-source --verify-source against PNT+ 21998bb6196b56789f72a52656a781a75e134eb0
  • --inspect-source report validated
  • --require-classified rejects the expected 449 pending records
  • copyright, line-count, DAG, trust-surface, Phase 4, conformance registration, factor freshness, and diff checks pass
  • fresh exact-head Opus review: merge-ready, no blockers

No Lean sources or proof trust mechanisms change in this PR.

@kim-em
kim-em merged commit 23c4e00 into main Aug 14, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant