feat(interval): replay pinned PNT+ nested logarithm

[kim-em]

Summary

• accept PNT+ inventory record 404, LogTables.log_log_6_58_gt, from PrimeNumberTheoremAnd/IEANTN/LogTables.lean:141:63 at pinned PNT+ commit 21998bb6196b56789f72a52656a781a75e134eb0
• classify it accepted-after-rewrite: exact 329/50 source fact -> checked strict positive inner log enclosure -> checked outer lower bound -> ordinary theorem through the generic package/session/chronology/ProofFrontend path
• keep one reusable runtime log handler load-bearing across both events, including at shifted node positions; reject a zero-touching inner enclosure, missing inner source, bypassed dependency, wrong output node, and mismatched replay payloads
• retain Mathlib-free runtime planning and put Real.log semantics/Taylor remainder proofs in HexIntervalMathlib only; import no LeanCert

Exact base and audit

Final head 19f0c65 is one commit over exact main 22d293d. The inventory names Mathlib Real.abs_log_sub_add_sum_range_le at truncation orders 150 and 40 as the numeric provider.

The executable provider is deliberately a finite package-owned table. This PR does not claim an arbitrary-rational logarithm provider, general rational interval fact domain, runtime range reduction, or precision refinement. The outer proof consumes the checked positive inner assumption via log monotonicity. The final theorem has the expected standard Mathlib axioms guard only.

The planner-level zero-touching mutation deliberately removes the exact source fact; retaining it would allow the first rule to refine the mutation back to the positive inner table enclosure. Replay independently rejects the zero-touching assumption.

The lakefile change has an exact proof-only benchmark exemption from baseline blob 6dd80771ae2212333b2a9b925b52056e0037ff56 to final blob 85f3a799be1661b7624e63b28aa1f6996763d4e8 because it registers only interval experiments and conformance, outside the factorization service executable graph.

Verification

• lake build HexInterval.Experiment.PntNestedLog HexIntervalMathlib.Experiment.PntNestedLog HexIntervalMathlib.PntNestedLogConformance
• lake build HexIntervalExperiment HexIntervalMathlibExperiment HexConformance (9,377 jobs)
• pinned inventory check/source verification and 24 inventory tests
• benchmark freshness, release manifest/trust surface, DAG, conformance target, copyright/line-count, and diff checks
• published trust scan: 422 Lean files, no axioms, sorries, or native_decide