feat(interval): replay pinned PNT log two bounds

[kim-em]

Summary

• add a Mathlib-free watched-input package that emits a package-owned two-sided log 2 window only from the exact input fact x = 2
• interpret and replay that rule in HexIntervalMathlib, then close the pinned PNT+ log_2_gt and log_2_lt statements through the generic TargetRun → chronology → ProofFrontend.emitTrace → closeTarget path
• reject mutated payloads, assumptions, nodes, and facts; include an unknown-input saturation canary, an offset-node runtime/schema canary, and an exact #print axioms guard
• classify the two exact records from PNT+ commit 21998bb6196b56789f72a52656a781a75e134eb0 as replaced-by-stronger-result, with required replacement fields naming Mathlib Real.log_two_gt_d9 and Real.log_two_lt_d9; reseal the inventory record digest
• require repo-relative proof evidence in finished inventory classifications to name an existing file, with a missing-path mutation test

This is deliberately an integration probe, not a generic logarithm or Taylor-series implementation. The SPEC explicitly excludes it from the arbitrary-input, nested-log, high-accuracy table, range-reduction, batching, and cache milestones. No LeanCert module is imported.

Audit and classification

• exact pinned declarations: PrimeNumberTheoremAnd.LogTables.log_2_gt and log_2_lt
• exact source pin: PNT+ 21998bb6196b56789f72a52656a781a75e134eb0
• classification: replaced-by-stronger-result, because Mathlib's kernel theorems prove the strict stronger decimal bounds 0.6931471803 < Real.log 2 and Real.log 2 < 0.6931471808
• ordinary Hex theorem: HexIntervalMathlib.Experiment.PntLogTable.pntLogTwo; the inventory evidence names its conformance file and each exact numerical provider
• trust guard: exact #print axioms output is [propext, Classical.choice, Quot.sound]; no axiom, sorry, or native_decide
• inventory digest independently resealed by the checker; no audit record or corpus count was changed

Verification

• lake build HexIntervalMathlib.PntLogTableConformance
• python3 -m unittest scripts.maintenance.test_pnt_inventory (24 tests)
• python3 scripts/maintenance/pnt_inventory.py --check
• python3 scripts/maintenance/pnt_inventory.py --verify-source --source /tmp/pnt-survey.ih3erF
• python3 scripts/bench/check_factor_sweep_freshness.py
• python3 scripts/plots/hexbz-cactus.py --check (25 committed figures current)
• copyright, tracked line-count, import DAG, released-manifest, manual-split, trust-surface, Phase 4, and conformance-target checks
• no axiom, sorry, or native_decide in the three new Lean files

The only factorization freshness-surface change is lakefile.lean registering these interval experiment/conformance modules. Its exact measured-baseline/current blob pair is recorded in proof_only_runtime_exemptions.json; the factorization executable and dependency graph are unchanged.

Based on exact current main 51c97d7d5f50c15bca48ee6a16bc6c52c6579a16 (including #9221 and #9222).