diff --git a/HexInterval/Experiment/PntLogTable.lean b/HexInterval/Experiment/PntLogTable.lean
new file mode 100644
index 000000000..9e0b83d34
--- /dev/null
+++ b/HexInterval/Experiment/PntLogTable.lean
@@ -0,0 +1,196 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import HexInterval.Experiment.PolicySession
+
+@[expose] public section
+
+/-!
+# Mathlib-free PNT+ logarithm-table probe
+
+This package is a deliberately small acceptance vertical for the first two
+entries of PNT+'s pinned `LogTables.lean`: the lower and upper bounds on
+`log 2`.  The executable side knows neither real logarithms nor decimal
+semantics.  It only propagates a package-owned finite fact from an exact-input
+fact.  `HexIntervalMathlib` supplies and checks the mathematical meaning.
+
+The finite fact domain is intentionally local to the probe.  It demonstrates
+the generic watched-input planning and replay boundary without pretending to
+be the eventual arbitrary-precision dyadic logarithm package.
+-/
+
+namespace Hex.Interval.Experiment.PntLogTable
+
+open Propagator PayloadArena
+
+/-- Facts needed by the source-pinned `log 2` acceptance probe. -/
+inductive Bound where
+  | all
+  | two
+  | logTwoWindow
+  | empty
+  deriving DecidableEq, Repr
+
+namespace Bound
+
+/-- Exact intersection for the probe's finite fact lattice. -/
+def meet : Bound → Bound → Bound
+  | .empty, _ | _, .empty => .empty
+  | .all, right => right
+  | left, .all => left
+  | .two, .two => .two
+  | .logTwoWindow, .logTwoWindow => .logTwoWindow
+  | .two, .logTwoWindow | .logTwoWindow, .two => .empty
+
+def code : Bound → Nat
+  | .all => 0
+  | .two => 1
+  | .logTwoWindow => 2
+  | .empty => 3
+
+def ofCode? : Nat → Option Bound
+  | 0 => some .all
+  | 1 => some .two
+  | 2 => some .logTwoWindow
+  | 3 => some .empty
+  | _ => none
+
+end Bound
+
+def factDomain : FactDomain Bound where
+  top _ := .all
+  narrow _ current proposed :=
+    let installed := current.meet proposed
+    if installed == current then .noChange
+    else if installed == .empty then .contradiction installed
+    else .improved installed
+
+def real : DomainId := { index := 0 }
+
+def sourceKey : OpKey := { name := "pnt-log-table.source" }
+def logKey : OpKey := { name := "pnt-log-table.log" }
+def logRuleKey : RuleKey := { name := "pnt-log-table.log-two" }
+
+def sourceOperation : Operation :=
+  { key := sourceKey, inputs := [], output := real }
+
+def logOperation : Operation :=
+  { key := logKey, inputs := [real], output := real }
+
+def operations : Array Operation := #[sourceOperation, logOperation]
+
+def node (index : Nat) : NodeId := { index }
+def payload (index : Nat) : PayloadId := { index }
+
+def sourceInstruction : Node :=
+  { domain := real, op := { index := 0 }, args := [] }
+
+def logInstruction : Node :=
+  { domain := real, op := { index := 1 }, args := [node 0] }
+
+/-- Caller graph for the closed expression `Real.log 2`. -/
+def program : Program :=
+  { operations, nodes := #[sourceInstruction, logInstruction] }
+
+def logRule : Registration :=
+  { key := logRuleKey
+    head := logKey
+    kind := .forward
+    watches := [.argument 0]
+    writes := [.result] }
+
+def factFormat : ReplayFormat :=
+  { role := .fact
+    schema := 1
+    validateBody := fun body =>
+      match body with
+      | [code] => Bound.ofCode? code == some .logTwoWindow
+      | _ => false }
+
+/-- The source-pinned table entry applies only when the watched input is
+known to be exactly two. -/
+def logPlan (request : RuleRequest Bound) : Plan Bound :=
+  match request.inputs, request.writes with
+  | [input], [target] =>
+      if input.fact == .two then
+        { outcome :=
+            .success
+              [{ node := target, fact := .logTwoWindow, payload := payload 0 }]
+              [] { arithmeticWork := 1, estimatedProofNodes := 1 }
+          drafts :=
+            [{ label := payload 0
+               role := .fact
+               schema := 1
+               body := [Bound.logTwoWindow.code] }] }
+      else
+        { outcome := .noChange {}, drafts := [] }
+  | _, _ => { outcome := .failed 1, drafts := [] }
+
+def sourcePackage : Package Bound :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation]
+    handlers := #[] }
+
+def logPackage : Package Bound :=
+  { Cache := Unit
+    cache := ()
+    operations := #[logOperation]
+    handlers := #[Handler.statelessPlanned logRule logPlan #[factFormat]] }
+
+def packages : Array (Package Bound) := #[sourcePackage, logPackage]
+
+def engineLimits : Propagator.Limits :=
+  { maxOperations := 2
+    maxNodes := 3
+    maxRules := 1
+    maxRegistryEntries := 8
+    maxReplayFormats := 2
+    maxArity := 1
+    maxScopeNodes := 1
+    maxApplications := 2
+    maxQueueEntries := 8
+    maxActions := 4
+    maxMatcherVisits := 2
+    matcherBatchSize := 2
+    maxAcceptedFacts := 2
+    maxRetainedSuggestions := 0
+    maxEffort := 0
+    maxObservationValue := 8
+    maxDiagnosticValue := 300
+    maxOutcomeCandidates := 1
+    maxOutcomeSuggestions := 0
+    maxProposalItems := 1
+    maxInstances := 0
+    maxGeneration := 0
+    maxNodeDepth := 2
+    maxEqualities := 0
+    splitEndpointLimit :=
+      { maxEndpointHeight := 8, maxAlignmentShift := 4 } }
+
+def policyLimits : Propagator.Policy.Limits :=
+  { maxDecisions := 8
+    maxTraversal := 32
+    maxLiveOffers := 8 }
+
+def arenaLimits : PayloadArena.Limits :=
+  { maxEntries := 4
+    maxBodyCells := 4
+    maxDrafts := 2
+    maxDraftCells := 2
+    maxAtom := 8
+    maxSchema := 1
+    maxUses := 2 }
+
+def limits : PolicySession.Limits :=
+  { engine := engineLimits, policy := policyLimits, arena := arenaLimits }
+
+def start : Except PolicySession.StartError (PolicySession.Session Bound) :=
+  PolicySession.Session.start factDomain program packages #[.two, .all] limits
+
+end Hex.Interval.Experiment.PntLogTable
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 632b18dbb..d7c6314f8 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -3208,6 +3208,16 @@ generic expression search.
 
 #### Certified logarithm tables
 
+The initial source-pinned PNT+ probe is intentionally narrower than this
+table-building target. A Mathlib-free package recognizes the exact input fact
+for `2` and emits a package-owned opaque fact through the generic policy
+session. Its Mathlib companion interprets that fact as PNT+'s six-decimal
+two-sided `log 2` window and replays the event from stronger existing Mathlib
+point bounds. This validates exact-input dependency, package-owned fact replay,
+and ordinary theorem closure. It is not a generic logarithm propagator, does
+not compute a series, and does not satisfy any of the precision, batching,
+ordering, or cache requirements below.
+
 The table-building acceptance program constructs enclosures for
 
 `Real.log (1 + (i : ℝ) / 256)`, for every `i : ℕ` with `i ≤ 256`,
diff --git a/HexIntervalMathlib/Experiment/PntLogTable.lean b/HexIntervalMathlib/Experiment/PntLogTable.lean
new file mode 100644
index 000000000..ecf3645e6
--- /dev/null
+++ b/HexIntervalMathlib/Experiment/PntLogTable.lean
@@ -0,0 +1,241 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import Mathlib.Analysis.Complex.ExponentialBounds
+public import Mathlib.Tactic.NormNum
+public import HexInterval.Experiment.PntLogTable
+public import HexInterval.Experiment.ProofRegistry
+public import HexInterval.Experiment.OperationSemantics
+
+@[expose] public section
+
+/-!
+# Real semantics for the PNT+ logarithm-table probe
+
+The Mathlib-free package propagates an opaque `logTwoWindow` fact.  This
+companion interprets it as PNT+'s pinned six-decimal bounds and proves the
+corresponding replay schema from Mathlib's stronger kernel-checked bounds.
+No LeanCert definition or theorem is imported.
+-/
+
+namespace Hex.Interval.Experiment.PntLogTable
+
+open Propagator SemanticReplay ChronologicalReplay ProofEmitter ProofRegistry
+open GenericInstanceReconstruction OperationSemantics
+
+/-- Mathematical meaning of the probe's finite facts. -/
+def Contains : Bound → ℝ → Prop
+  | .all, _ => True
+  | .two, x => x = 2
+  | .logTwoWindow, x => (0.693147 : ℝ) < x ∧ x < 0.693148
+  | .empty, _ => False
+
+def sourceModel : OperationSemantics.Model ℝ :=
+  { operation := sourceOperation
+    relation := fun inputs _ => inputs = [] }
+
+def logModel : OperationSemantics.Model ℝ :=
+  { operation := logOperation
+    relation := fun inputs output =>
+      match inputs with
+      | [input] => output = Real.log input
+      | _ => False }
+
+def operationModels : Array (OperationSemantics.Model ℝ) :=
+  #[sourceModel, logModel]
+
+def semantics : Semantics Bound :=
+  OperationSemantics.semantics operationModels Contains
+
+theorem containsMeet (left right : Bound) (x : ℝ) :
+    Contains (left.meet right) x ↔ Contains left x ∧ Contains right x := by
+  cases left <;> cases right <;> simp [Bound.meet, Contains]
+  · intro equal _
+    subst x
+    norm_num
+  · intro _ upper equal
+    subst x
+    norm_num at upper
+
+def boundSchema : FactDomainSchema semantics :=
+  { top := fun _ => .all
+    topSound := by
+      intro _ _ _ _ _ _
+      trivial
+    proveMeet := fun _ _ previous proposed installed =>
+      if exact : installed = previous.meet proposed then
+        some
+          { proof := by
+              subst installed
+              intro valuation _
+              exact containsMeet previous proposed (valuation _) }
+      else
+        none }
+
+def laws : Laws semantics :=
+  { holdsEq := by
+      intro _ valuation left right fact _ _ values
+      change Contains fact (valuation left) ↔ Contains fact (valuation right)
+      rw [values] }
+
+/-- Semantic theorem for the package-owned table entry.  The watched input
+fact is load-bearing: replay first recovers that the argument is exactly two,
+then applies Mathlib's stronger decimal-nine theorems. -/
+theorem logEntails (graph : Program) (assumptions : List (NodeFact Bound))
+    (output : NodeId) (instruction : Node) (input : NodeId)
+    (found : graph.node? output = some instruction)
+    (operation : instruction.op = { index := 1 })
+    (arguments : instruction.args = [input])
+    (inputFacts : assumptions = [{ node := input, fact := .two }]) :
+    semantics.Entails graph assumptions
+      { node := output, fact := .logTwoWindow } := by
+  change ∀ valuation : NodeId → ℝ,
+    OperationSemantics.Models operationModels graph valuation →
+      (∀ assumption, assumption ∈ assumptions →
+        Contains assumption.fact (valuation assumption.node)) →
+      Contains .logTwoWindow (valuation output)
+  intro valuation model holds
+  have inputIsTwo : valuation input = 2 := by
+    have exactInput := holds { node := input, fact := .two } (by simp [inputFacts])
+    exact exactInput
+  obtain ⟨meaning, meaningAt, related⟩ := model.2 output instruction found
+  simp [operationModels, operation] at meaningAt
+  subst meaning
+  have outputEq : valuation output = Real.log (valuation input) := by
+    simpa [logModel, arguments, List.map] using related
+  rw [outputEq, inputIsTwo]
+  constructor
+  · exact (by
+      have stronger := Real.log_two_gt_d9
+      norm_num at stronger ⊢
+      linarith)
+  · exact (by
+      have stronger := Real.log_two_lt_d9
+      norm_num at stronger ⊢
+      linarith)
+
+private theorem factWith {Fact : Type} (fact : NodeFact Fact) {value : Fact}
+    (equal : fact.fact = value) :
+    fact = { node := fact.node, fact := value } := by
+  cases fact
+  simp_all
+
+def logFactSchema : PackedFactSchema semantics where
+  rule := logRuleKey
+  schema := 1
+  Certificate := Unit
+  decode := fun body =>
+    if body == [Bound.logTwoWindow.code] then some () else none
+  replay := fun _ _ context _ =>
+    if proposedFact : context.proposed.fact = .logTwoWindow then
+      match found : context.program.node? context.proposed.node with
+      | some instruction =>
+          if operation : instruction.op = ({ index := 1 } : OpId) then
+            match arguments : instruction.args with
+            | [input] =>
+                if inputFacts : context.assumptions =
+                    [{ node := input, fact := .two }] then
+                  some
+                    { proof := by
+                        have proposedEq :
+                            context.proposed =
+                              { node := context.proposed.node,
+                                fact := .logTwoWindow } := by
+                          exact factWith context.proposed proposedFact
+                        rw [proposedEq]
+                        exact
+                          logEntails context.program context.assumptions
+                            context.proposed.node instruction input found
+                            operation arguments inputFacts }
+                else
+                  none
+            | _ => none
+          else
+            none
+      | none => none
+    else
+      none
+
+def stableLaw : StableLaw semantics :=
+  OperationSemantics.stableLaw operationModels Contains
+
+def sourceEmit : EmitPackage Lean.Name := { schemas := [] }
+
+def logEmit : EmitPackage Lean.Name :=
+  { schemas :=
+      [{ key := logFactSchema.key
+         handle := ``logFactSchema }] }
+
+def sourceProof : ProofRegistry.Package semantics Lean.Name :=
+  { semantic := { factSchemas := #[] }
+    emit := sourceEmit }
+
+def logProof : ProofRegistry.Package semantics Lean.Name :=
+  { semantic := { factSchemas := #[logFactSchema] }
+    emit := logEmit }
+
+def proofPackages : Array (ProofRegistry.Package semantics Lean.Name) :=
+  #[sourceProof, logProof]
+
+def baseFacts : List (NodeFact Bound) :=
+  [{ node := node 0, fact := .two }, { node := node 1, fact := .all }]
+
+def checkerInput : CheckerInput Bound :=
+  { baseProgram := program
+    initialFacts := #[.two, .all]
+    target := { node := node 1, fact := .logTwoWindow } }
+
+theorem baseWithin : FactsWithin program baseFacts := by
+  intro fact member
+  simp only [baseFacts, List.mem_cons, List.not_mem_nil, or_false] at member
+  rcases member with rfl | rfl <;> simp [program, node]
+
+theorem basePrefix : ProgramPrefix program program :=
+  ProgramPrefix.refl program
+
+theorem sameOperations : program.operations = program.operations := rfl
+
+def initialExtension : Evidence (semantics.Extends program program) :=
+  extendRefl semantics program
+
+noncomputable def valuation : NodeId → ℝ
+  | ⟨0⟩ => 2
+  | ⟨1⟩ => Real.log 2
+  | _ => 0
+
+theorem valuationModels : semantics.models program valuation := by
+  refine ⟨?_, ?_⟩
+  · simp [program, operations, operationModels, sourceModel, logModel]
+  rintro ⟨index⟩ instruction found
+  cases index with
+  | zero =>
+      simp [Program.node?, program, sourceInstruction] at found
+      subst instruction
+      exact ⟨sourceModel, by rfl, by rfl⟩
+  | succ index =>
+      cases index with
+      | zero =>
+          simp [Program.node?, program, logInstruction] at found
+          subst instruction
+          exact ⟨logModel, by rfl, by rfl⟩
+      | succ index =>
+          simp [Program.node?, program] at found
+
+/-- Close emitted generic evidence to the two ordinary PNT+ statements. -/
+theorem closeLogTwo
+    (result : Evidence
+      (semantics.Entails program baseFacts checkerInput.target)) :
+    (0.693147 : ℝ) < Real.log 2 ∧ Real.log 2 < 0.693148 := by
+  exact result.proof valuation valuationModels (by
+    intro fact member
+    simp only [baseFacts, List.mem_cons, List.not_mem_nil, or_false] at member
+    rcases member with rfl | rfl
+    · rfl
+    · trivial)
+
+end Hex.Interval.Experiment.PntLogTable
diff --git a/SPEC/Libraries/hex-interval-mathlib.md b/SPEC/Libraries/hex-interval-mathlib.md
index 2ade0c763..9bb53690a 100644
--- a/SPEC/Libraries/hex-interval-mathlib.md
+++ b/SPEC/Libraries/hex-interval-mathlib.md
@@ -1047,8 +1047,29 @@ accepted fixture, documented rewrite, stronger replacement theorem, retained
 dependency, or expected-failure fixture as appropriate. The release claim
 requires both this classified manifest and the referenced ported proofs; a
 status label alone cannot establish coverage. The inventory checker validates
-that evidence references are structured and nonempty; the release profile must
-also build and axiom-audit the referenced proof fixtures.
+that evidence references are structured and nonempty and that repo-relative
+proof paths exist; the release profile must also build and axiom-audit the
+referenced proof fixtures.
+
+The first classified acceptance probe covers the pinned declarations
+`LogTables.log_2_gt` and `LogTables.log_2_lt`. The Mathlib-free
+`PntLogTable` package watches an exact-input fact for `2`, runs the generic
+policy session, and emits one package-owned two-sided-window fact. Its Mathlib
+companion interprets the opaque logarithm operation, checks the stronger
+`Real.log_two_gt_d9` and `Real.log_two_lt_d9` theorems, and replays the exact
+event through `ProofFrontend` before closing the original six-decimal
+conjunction as an ordinary theorem. Conformance rejects a changed payload,
+input assumption, output node, or output fact and audits the closed theorem's
+axioms. These two records are classified as replacements by stronger numerical
+provider results, with the exact Mathlib theorem recorded explicitly; no
+LeanCert declaration is imported.
+
+This probe establishes the package/planning/replay path, not the eventual
+numerical logarithm algorithm. Its four-element finite fact lattice and its
+reuse of Mathlib's existing point bounds are deliberately local. It does not
+satisfy the high-accuracy table, arbitrary input, nested-logarithm, range
+reduction, or package-owned Taylor-series milestones, and must not be counted
+as evidence for those records.
 
 Refreshing an upstream pin must regenerate and review the manifest. The
 inventory prevents blind spots; it does not make exact-source compatibility a
diff --git a/conformance-fixtures/HexIntervalMathlib/pnt-inventory.jsonl b/conformance-fixtures/HexIntervalMathlib/pnt-inventory.jsonl
index fc1f30faf..b1e9edfe1 100644
--- a/conformance-fixtures/HexIntervalMathlib/pnt-inventory.jsonl
+++ b/conformance-fixtures/HexIntervalMathlib/pnt-inventory.jsonl
@@ -1,4 +1,4 @@
-{"audit_record_digest":"6cfed911ea5dc11a114be8cadad83aaf1a68972a166700ceea894a7145e2d07d","counts":{"bklnw_table10_a2_sites":38,"bklnw_table10_target_sites":87,"bklnw_table12_checks":130,"bklnw_table12_logarithmic_rows":2,"bklnw_table12_ordinary_rows":24,"dependency_interface":6,"fks2_cells":13590,"fks2_shards":14,"interval_auto_actual":60,"interval_auto_textual":61,"interval_decide_actual":280,"interval_decide_textual":290,"leancert_import":16,"leancert_reference":107,"native_decide_actual":83,"records":567},"format":1,"kind":"meta","lean_source_digest":"84b1cdfe1cae7b6ddc181aede13c35b276422a206f6815143c2a1c50c3c0b112","lean_source_files":232,"pins":{"lean_toolchain":"leanprover/lean4:v4.32.2","leancert":"58edbea59458e9b010262238eaca27b6e0240dae","mathlib":"905b95818eb32af7874a58b427f50c1711a5e96c","pnt":"21998bb6196b56789f72a52656a781a75e134eb0"},"record_digest":"a86c79de333d3cae4f6818e4d2401ca646da81b2243b3dbc13676284ae953ba9"}
+{"audit_record_digest":"6cfed911ea5dc11a114be8cadad83aaf1a68972a166700ceea894a7145e2d07d","counts":{"bklnw_table10_a2_sites":38,"bklnw_table10_target_sites":87,"bklnw_table12_checks":130,"bklnw_table12_logarithmic_rows":2,"bklnw_table12_ordinary_rows":24,"dependency_interface":6,"fks2_cells":13590,"fks2_shards":14,"interval_auto_actual":60,"interval_auto_textual":61,"interval_decide_actual":280,"interval_decide_textual":290,"leancert_import":16,"leancert_reference":107,"native_decide_actual":83,"records":567},"format":1,"kind":"meta","lean_source_digest":"84b1cdfe1cae7b6ddc181aede13c35b276422a206f6815143c2a1c50c3c0b112","lean_source_files":232,"pins":{"lean_toolchain":"leanprover/lean4:v4.32.2","leancert":"58edbea59458e9b010262238eaca27b6e0240dae","mathlib":"905b95818eb32af7874a58b427f50c1711a5e96c","pnt":"21998bb6196b56789f72a52656a781a75e134eb0"},"record_digest":"5d4987c9ac7093bfbdaa524409133b5cbe8566316fbca098a0842498e54a176f"}
 {"import_sites":[{"line":2,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean"}],"kind":"dependency-interface","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.ANT","role":"whole-interval ANT expression checker used by the extended FKS2 table","workload":"fks2-table4ext"}
 {"import_sites":[{"line":7,"path":"PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_a2_bounds.lean"}],"kind":"dependency-interface","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.CertifiedBounds.BKLNW","role":"certified exponential and power bounds used by the BKLNW sums","workload":"bklnw-certified-bounds"}
 {"import_sites":[{"line":9,"path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean"},{"line":3,"path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean"},{"line":2,"path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean"}],"kind":"dependency-interface","migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"module":"LeanCert.CertifiedBounds.Chebyshev","role":"certified Chebyshev bounds used by Chebyshev, FKS2 floor, and Ramanujan proofs","workload":"chebyshev-certified-bounds"}
@@ -365,8 +365,8 @@
 {"actual":true,"column":56,"declaration":"kadiri_lumley_odd_goldbach_finite","kind":"tactic-occurrence","line":250,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","snippet":"have : Real.exp 59 + 4 + 1 \u2264 11325 * 10 ^ 22 := by interval_decide","tactic":"interval_decide"}
 {"actual":true,"column":69,"declaration":"kadiri_lumley_odd_goldbach_finite","kind":"tactic-occurrence","line":267,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","snippet":"have : Real.exp 60 + 4 + 1 \u2264 7785131284000000000000000004 := by interval_decide","tactic":"interval_decide"}
 {"actual":false,"column":37,"declaration":null,"kind":"tactic-occurrence","line":5,"migration":{"status":"not-a-call"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"Each bound is proved by LeanCert's `interval_decide` tactic (verified Taylor series).","tactic":"interval_decide"}
-{"actual":true,"column":41,"declaration":"log_2_gt","kind":"tactic-occurrence","line":15,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_2_gt : 0.693147 < log 2 := by interval_decide","tactic":"interval_decide"}
-{"actual":true,"column":41,"declaration":"log_2_lt","kind":"tactic-occurrence","line":16,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_2_lt : log 2 < 0.693148 := by interval_decide","tactic":"interval_decide"}
+{"actual":true,"column":41,"declaration":"log_2_gt","kind":"tactic-occurrence","line":15,"migration":{"evidence":["Hex.IntervalMathlib.PntLogTableConformance.pntLogTwo","conformance/HexIntervalMathlib/PntLogTableConformance.lean"],"note":"Generic Hex watched-input planning and kernel replay prove the pinned lower bound without importing LeanCert; Mathlib supplies the stronger numerical point theorem.","numeric_provider":"Mathlib Real.log_two_gt_d9","replacement":"Mathlib Real.log_two_gt_d9, narrowed and replayed by Hex.IntervalMathlib.PntLogTableConformance.pntLogTwo","status":"replaced-by-stronger-result"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_2_gt : 0.693147 < log 2 := by interval_decide","tactic":"interval_decide"}
+{"actual":true,"column":41,"declaration":"log_2_lt","kind":"tactic-occurrence","line":16,"migration":{"evidence":["Hex.IntervalMathlib.PntLogTableConformance.pntLogTwo","conformance/HexIntervalMathlib/PntLogTableConformance.lean"],"note":"Generic Hex watched-input planning and kernel replay prove the pinned upper bound without importing LeanCert; Mathlib supplies the stronger numerical point theorem.","numeric_provider":"Mathlib Real.log_two_lt_d9","replacement":"Mathlib Real.log_two_lt_d9, narrowed and replayed by Hex.IntervalMathlib.PntLogTableConformance.pntLogTwo","status":"replaced-by-stronger-result"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_2_lt : log 2 < 0.693148 := by interval_decide","tactic":"interval_decide"}
 {"actual":true,"column":41,"declaration":"log_3_gt","kind":"tactic-occurrence","line":18,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_3_gt : 1.098612 < log 3 := by interval_decide","tactic":"interval_decide"}
 {"actual":true,"column":41,"declaration":"log_3_lt","kind":"tactic-occurrence","line":19,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_3_lt : log 3 < 1.098613 := by interval_decide","tactic":"interval_decide"}
 {"actual":true,"column":41,"declaration":"log_5_gt","kind":"tactic-occurrence","line":21,"migration":{"note":"D8 migration decision not yet assigned","status":"pending"},"path":"PrimeNumberTheoremAnd/IEANTN/LogTables.lean","snippet":"lemma log_5_gt : 1.609437 < log 5 := by interval_decide","tactic":"interval_decide"}
diff --git a/conformance/HexIntervalMathlib/PntLogTableConformance.lean b/conformance/HexIntervalMathlib/PntLogTableConformance.lean
new file mode 100644
index 000000000..8ec18c095
--- /dev/null
+++ b/conformance/HexIntervalMathlib/PntLogTableConformance.lean
@@ -0,0 +1,265 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+import HexIntervalMathlib.Experiment.PntLogTable
+import HexInterval.Experiment.ProofFrontend
+import HexInterval.Experiment.TargetRun
+import Mathlib.Lean.Elab.Tactic.Meta
+
+/-!
+# Source-pinned PNT+ logarithm acceptance probe
+
+This fixture covers `LogTables.log_2_gt` and `LogTables.log_2_lt` from PNT+
+commit `21998bb6196b56789f72a52656a781a75e134eb0`.  Search runs the ordinary
+Mathlib-free watched-input package.  Proof emission replays its one-event
+chronology through the package schema and closes the original real theorem.
+-/
+
+namespace Hex.IntervalMathlib.PntLogTableConformance
+
+open Lean Elab Tactic Meta
+open Hex.Interval.Experiment
+open Propagator PolicySession SemanticReplay ChronologicalReplay ProofEmitter
+open Frontend ProofFrontend ProofRegistry PntLogTable
+
+private def firstOffer : TargetRun.Controller Bound Unit :=
+  { update := fun state _ => state
+    choose := fun state view =>
+      match view.offers[0]? with
+      | some offer => .select offer state
+      | none => .stop state }
+
+private def run? (input : CheckerInput Bound) :
+    Option (TargetRun.Result Bound Unit) := do
+  let .ok session := PolicySession.Session.start factDomain input.baseProgram
+      packages input.initialFacts limits
+    | none
+  some (TargetRun.drive factDomain input.target.node input.target.fact
+    firstOffer limits.policy.maxDecisions session ())
+
+structure Fixture where
+  session : PolicySession.Session Bound
+  registry : ProofRegistry.Registry semantics Lean.Name
+  reached : TargetRun.Reached Bound
+  events : Array (TargetRun.Event Bound)
+
+def fixture? : Option Fixture := do
+  let result ← run? checkerInput
+  let .target reached := result.stop | none
+  let .ok registry := ProofRegistry.build result.session.registry proofPackages
+    | none
+  some
+    { session := result.session
+      registry
+      reached
+      events := result.events }
+
+#guard
+  fixture?.any fun fixture =>
+    fixture.reached.seen == ({ node := node 1, version := 1 } : SeenVersion) &&
+      fixture.reached.fact == .logTwoWindow && fixture.events.size == 1 &&
+      fixture.session.state.engine.facts == #[.two, .logTwoWindow] &&
+      fixture.session.state.engine.chronology == #[.fact 0] &&
+      fixture.registry.emit.find? logFactSchema.key == some ``logFactSchema
+
+#guard
+  baseFacts ==
+      [{ node := node 0, fact := .two }, { node := node 1, fact := .all }] &&
+    checkerInput.initialFacts == #[.two, .all]
+
+private def unknownInput : CheckerInput Bound :=
+  { checkerInput with initialFacts := #[.all, .all] }
+
+-- The executable package must not produce a numerical window without the
+-- exact-input fact used by its theorem schema.
+#guard
+  (run? unknownInput).any fun result =>
+    match result.stop with
+    | .saturated =>
+        result.events.size == 1 &&
+          result.session.state.engine.facts == #[.all, .all] &&
+          result.session.state.engine.chronology.isEmpty
+    | _ => false
+
+private def offsetInstruction : Node :=
+  { domain := real, op := { index := 1 }, args := [node 0] }
+
+private def offsetProgram : Program :=
+  { operations
+    nodes := #[sourceInstruction, sourceInstruction, offsetInstruction] }
+
+private def offsetInput : CheckerInput Bound :=
+  { baseProgram := offsetProgram
+    initialFacts := #[.two, .all, .all]
+    target := { node := node 2, fact := .logTwoWindow } }
+
+-- The same package route is not tied to node one of the two-node fixture.
+#guard
+  (run? offsetInput).any fun result =>
+    match result.stop with
+    | .target reached =>
+        reached.seen == ({ node := node 2, version := 1 } : SeenVersion) &&
+          reached.fact == .logTwoWindow && result.events.size == 1 &&
+          result.session.state.engine.facts ==
+            #[.two, .all, .logTwoWindow]
+    | _ => false
+
+private def offsetAction : Action :=
+  { serial := 0
+    programVersion := 0
+    application := { index := 0 }
+    rule := { index := 0 }
+    key := logRuleKey
+    node := node 2
+    kind := .forward
+    effort := 0
+    generation := 0
+    inputs := []
+    writes := [node 2] }
+
+private def offsetContext : RuleFactContext offsetInput offsetAction :=
+  { program := offsetProgram
+    basePrefix := ProgramPrefix.refl offsetProgram
+    assumptions := [{ node := node 0, fact := .two }]
+    proposed := { node := node 2, fact := .logTwoWindow } }
+
+#guard
+  (logFactSchema.replay offsetInput offsetAction offsetContext ()).isSome
+
+def trace? : Option (Frontend.Trace Bound) := do
+  match fixture? with
+  | none => none
+  | some fixture =>
+      Frontend.trace? fixture.session.state.engine fixture.session.arena
+
+#guard
+  trace?.any fun trace =>
+    trace.program == program &&
+      match trace.events with
+      | [.rule step] =>
+          step.entry.replayKey == logFactSchema.key &&
+            step.event.programVersion == 0 && step.event.node == node 1 &&
+            step.event.previous == ({ node := node 1, version := 0 } : SeenVersion) &&
+            step.event.fact == .logTwoWindow && step.event.version == 1 &&
+            step.assumptions == [{ node := node 0, fact := .two }] &&
+            step.previous == .all
+      | _ => false
+
+/-! ## Replay mutation rejection -/
+
+private def action : Action :=
+  { serial := 0
+    programVersion := 0
+    application := { index := 0 }
+    rule := { index := 0 }
+    key := logRuleKey
+    node := node 1
+    kind := .forward
+    effort := 0
+    generation := 0
+    inputs := []
+    writes := [node 1] }
+
+private def replayContext : RuleFactContext checkerInput action :=
+  { program
+    basePrefix := ProgramPrefix.refl program
+    assumptions := [{ node := node 0, fact := .two }]
+    proposed := { node := node 1, fact := .logTwoWindow } }
+
+#guard (logFactSchema.decode [Bound.logTwoWindow.code]).isSome
+#guard (logFactSchema.decode [Bound.all.code]).isNone
+#guard factFormat.validateBody [Bound.logTwoWindow.code]
+#guard !factFormat.validateBody [Bound.logTwoWindow.code, 99]
+#guard (logFactSchema.replay checkerInput action replayContext ()).isSome
+
+private def wrongInput : RuleFactContext checkerInput action :=
+  { replayContext with assumptions := [{ node := node 0, fact := .all }] }
+
+private def wrongOutput : RuleFactContext checkerInput action :=
+  { replayContext with proposed := { node := node 0, fact := .logTwoWindow } }
+
+private def wrongFact : RuleFactContext checkerInput action :=
+  { replayContext with proposed := { node := node 1, fact := .all } }
+
+#guard (logFactSchema.replay checkerInput action wrongInput ()).isNone
+#guard (logFactSchema.replay checkerInput action wrongOutput ()).isNone
+#guard (logFactSchema.replay checkerInput action wrongFact ()).isNone
+
+/-! ## Generic proof emission and ordinary theorem closure -/
+
+private def boundExpr : Bound → Expr
+  | .all => mkConst ``Bound.all
+  | .two => mkConst ``Bound.two
+  | .logTwoWindow => mkConst ``Bound.logTwoWindow
+  | .empty => mkConst ``Bound.empty
+
+private def boundEncoder : FrontendEncoder.Encoder Bound :=
+  FrontendEncoder.make (mkConst ``Bound) (fun fact => pure (boundExpr fact))
+
+private def seedAssumed (graph : Program) (base : List (NodeFact Bound))
+    (index : Nat) (fact : NodeFact Bound) (found : base[index]? = some fact) :
+    Evidence (semantics.Entails graph base fact) :=
+  ProofEmitter.assumedAt graph base index fact found
+
+private def frontendContext : ProofFrontend.Context Bound Name :=
+  { encoder := boundEncoder
+    resolveSchema := pure
+    semantics := mkConst ``semantics
+    domain := mkConst ``boundSchema
+    laws := mkConst ``laws
+    stableLaw := mkConst ``stableLaw
+    input := mkConst ``checkerInput
+    assumed := ``seedAssumed
+    baseFacts
+    baseFactsTerm := mkConst ``baseFacts
+    baseProgram := program
+    baseProgramTerm := mkConst ``program
+    basePrefix := mkConst ``basePrefix
+    baseWithin := mkConst ``baseWithin
+    initialExtension := mkConst ``initialExtension
+    finalPrefix := mkConst ``basePrefix
+    sameOperations := mkConst ``sameOperations
+    top := boundSchema.top }
+
+private meta def emitEvidence : MetaM Expr := do
+  let some fixture := fixture?
+    | throwError "pnt_log_table: search or proof registry failed"
+  let some trace := Frontend.trace? fixture.session.state.engine fixture.session.arena
+    | throwError "pnt_log_table: chronology quotation failed"
+  unless trace.program == program do
+    throwError "pnt_log_table: trace changed the expression graph"
+  let [.rule step] := trace.events
+    | throwError "pnt_log_table: expected exactly one rule event"
+  unless step.entry.replayKey == logFactSchema.key &&
+      step.assumptions == [{ node := node 0, fact := .two }] &&
+      step.event.node == node 1 && step.event.fact == .logTwoWindow do
+    throwError "pnt_log_table: emitted event drifted from the pinned probe"
+  let state ← ProofFrontend.emitTrace frontendContext trace.program trace.events
+    fixture.registry.emit
+  ProofFrontend.closeTarget frontendContext state fixture.reached.seen
+    fixture.reached.fact
+    checkerInput.target
+
+/-- The two pinned PNT+ `log 2` bounds, proved by generic Hex planning and
+schema replay and closed as an ordinary kernel theorem. -/
+theorem pntLogTwo :
+    (0.693147 : ℝ) < Real.log 2 ∧ Real.log 2 < 0.693148 := by
+  run_tac
+    let evidence ← emitEvidence
+    let proof ← mkAppM ``closeLogTwo #[evidence]
+    let goal ← getMainGoal
+    unless ← isDefEq (← inferType proof) (← goal.getType) do
+      throwError "pnt_log_table: closed replay has the wrong theorem"
+    goal.assign (← instantiateMVars proof)
+    replaceMainGoal []
+
+/--
+info: 'Hex.IntervalMathlib.PntLogTableConformance.pntLogTwo' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs in
+#print axioms pntLogTwo
+
+end Hex.IntervalMathlib.PntLogTableConformance
diff --git a/lakefile.lean b/lakefile.lean
index 30eb799f4..752e8ebb8 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -321,12 +321,14 @@ lean_lib HexIntervalExperiment where
     `HexInterval.Experiment.GoalClosure,
     `HexInterval.Experiment.TraceReplay,
     `HexInterval.Experiment.SineSign,
-    `HexInterval.Experiment.ExpSign]
+    `HexInterval.Experiment.ExpSign,
+    `HexInterval.Experiment.PntLogTable]
 
 lean_lib HexIntervalMathlibExperiment where
   globs := #[`HexIntervalMathlib.Experiment.Center,
     `HexIntervalMathlib.Experiment.SineSign,
-    `HexIntervalMathlib.Experiment.ExpSign]
+    `HexIntervalMathlib.Experiment.ExpSign,
+    `HexIntervalMathlib.Experiment.PntLogTable]
 
 lean_lib HexIntervalReplayProbe where
   srcDir := "bench"
@@ -390,7 +392,7 @@ lean_lib HexRCFProofProbeScientific where
 -- `*_emit_fixtures` exes below, carrying `srcDir := "conformance"`.
 lean_lib HexConformance where
   srcDir := "conformance"
-  globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.ScopeConformance, `HexInterval.StructuralMatcherConformance, `HexInterval.MatcherSchedulerConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexInterval.PolicySessionConformance, `HexInterval.PolicyFunctionConformance, `HexInterval.SemanticReplayConformance, `HexInterval.ChronologicalReplayConformance, `HexInterval.GenericInstanceReconstructionConformance, `HexInterval.ProofEmitterConformance, `HexInterval.TraceReplayConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.RefuteConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexMvPolyFixtures, `HexMvPoly.Conformance, `HexMvPolyMathlib.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one
+  globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.ScopeConformance, `HexInterval.StructuralMatcherConformance, `HexInterval.MatcherSchedulerConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexInterval.PolicySessionConformance, `HexInterval.PolicyFunctionConformance, `HexInterval.SemanticReplayConformance, `HexInterval.ChronologicalReplayConformance, `HexInterval.GenericInstanceReconstructionConformance, `HexInterval.ProofEmitterConformance, `HexInterval.TraceReplayConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.RefuteConformance, `HexIntervalMathlib.PntLogTableConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexMvPolyFixtures, `HexMvPoly.Conformance, `HexMvPolyMathlib.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one
 
 -- Public umbrellas intentionally contain only the supported API. Executable
 -- examples and regression tests are compiled through this separate target so
diff --git a/progress/20260814T145919Z.md b/progress/20260814T145919Z.md
new file mode 100644
index 000000000..586b13c99
--- /dev/null
+++ b/progress/20260814T145919Z.md
@@ -0,0 +1,45 @@
+# Accomplished
+
+- Added a Mathlib-free `PntLogTable` experiment that propagates a
+  package-owned two-sided `log 2` window only from an exact-input fact for `2`.
+- Added the Mathlib semantic companion and replay schema. The ordinary theorem
+  closes the pinned PNT+ six-decimal lower and upper bounds from the generic
+  policy-session chronology and stronger kernel-checked Mathlib bounds.
+- Added exact trace guards plus rejection checks for mutated payloads,
+  assumptions, nodes, and facts, and an exact `#print axioms` guard.
+- Added an executable unknown-input saturation canary, replayed the same schema
+  at a different graph node, routed the result through generic target closure,
+  and recorded the Mathlib numerical provider in each classified record.
+- Classified the pinned PNT+ `log_2_gt` and `log_2_lt` records as replacements
+  by stronger numerical-provider results, with structured evidence, and
+  resealed the inventory digest.
+- Documented the probe's deliberately narrow boundary in both interval SPECs:
+  it validates planning/replay, not a general logarithm or series algorithm.
+- Built `HexIntervalMathlib.PntLogTableConformance`, ran all 23 inventory unit
+  tests, validated the offline inventory, checked whitespace, and confirmed no
+  `axiom`, `sorry`, or `native_decide` appears in the new Lean files.
+- Recorded the exact `lakefile.lean` blob transition as proof-only and
+  runtime-neutral: it only registers interval experiment and conformance
+  modules, leaving the factorization executable graph unchanged.
+- Tightened the offline inventory audit so repo-relative proof evidence must
+  name an existing file, and added a mutation test for a missing evidence path.
+
+# Current frontier
+
+The first two executable PNT+ interval records now have a genuine Hex
+planning/replay proof rather than only inventory entries. The implementation
+uses a local finite fact lattice and Mathlib's existing stronger `log 2`
+theorems, so it is an integration canary rather than the numerical logarithm
+engine.
+
+# Next step
+
+Generalize the fact payload to exact dyadic endpoints and add a package-owned
+series or range-reduction provider, then cover `log 3` or a nested logarithm
+without relying on a pre-existing point-bound theorem.
+
+# Blockers
+
+No blocker for this probe. The general PNT+ logarithm and exponential corpus
+still needs an arbitrary-precision function provider; this commit deliberately
+does not claim that larger milestone.
diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json
index baefcf697..cf7a48604 100644
--- a/scripts/bench/proof_only_runtime_exemptions.json
+++ b/scripts/bench/proof_only_runtime_exemptions.json
@@ -143,6 +143,12 @@
     "current_blob": "30eb799f4c1194c115756da0d02d9027735ecb82",
     "reason": "Additionally registers Mathlib refutation conformance only; the factorization service target and executable dependency graph are unchanged."
   },
+  {
+    "path": "lakefile.lean",
+    "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
+    "current_blob": "752e8ebb8e814067aeb7d84301bffb1103cd1082",
+    "reason": "Additionally registers the Mathlib-free PNT log-two experiment, its Mathlib semantic companion, and its conformance module only; the factorization service target and executable dependency graph are unchanged."
+  },
   {
     "path": "HexBerlekamp/FactorTacticTests.lean",
     "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",
diff --git a/scripts/maintenance/pnt_inventory.py b/scripts/maintenance/pnt_inventory.py
index a5ebe523e..9aef89496 100644
--- a/scripts/maintenance/pnt_inventory.py
+++ b/scripts/maintenance/pnt_inventory.py
@@ -29,6 +29,7 @@
 from typing import Any, Iterable
 
 
+REPO_ROOT = Path(__file__).resolve().parents[2]
 PNT_COMMIT = "21998bb6196b56789f72a52656a781a75e134eb0"
 LEANCERT_COMMIT = "58edbea59458e9b010262238eaca27b6e0240dae"
 MATHLIB_COMMIT = "905b95818eb32af7874a58b427f50c1711a5e96c"
@@ -950,6 +951,16 @@ def require_migrations(records: list[dict[str, Any]]) -> None:
                 raise InventoryError(
                     f"record {index}: {status} requires nonempty evidence entries"
                 )
+            for item in evidence:
+                reference = item.split(":", 1)[0]
+                if "/" not in reference:
+                    continue
+                path = Path(reference)
+                if path.is_absolute() or ".." in path.parts \
+                        or not (REPO_ROOT / path).is_file():
+                    raise InventoryError(
+                        f"record {index}: evidence path does not exist: {reference}"
+                    )
             if status == "accepted-after-rewrite":
                 if not isinstance(migration.get("rewrite"), str) \
                         or not migration["rewrite"].strip():
@@ -1038,7 +1049,7 @@ def require_source_match(
 
 
 def default_fixture() -> Path:
-    return Path(__file__).resolve().parents[2] / (
+    return REPO_ROOT / (
         "conformance-fixtures/HexIntervalMathlib/pnt-inventory.jsonl"
     )
 
diff --git a/scripts/maintenance/test_pnt_inventory.py b/scripts/maintenance/test_pnt_inventory.py
index 8301678dc..d62d619b6 100644
--- a/scripts/maintenance/test_pnt_inventory.py
+++ b/scripts/maintenance/test_pnt_inventory.py
@@ -96,7 +96,9 @@ def test_classification_edits_do_not_change_audit_identity(self) -> None:
             "status": "accepted-after-rewrite",
             "note": "unit-test classification",
             "rewrite": "factor the repeated bound through one shared theorem",
-            "evidence": ["conformance/HexIntervalMathlib/PNTConformance.lean:example"],
+            "evidence": [
+                "conformance/HexIntervalMathlib/PntLogTableConformance.lean"
+            ],
         }
         path = self.write_rows(meta, records)
         inventory.update_classifications(path)
@@ -211,6 +213,18 @@ def test_finished_classification_requires_structured_evidence(self) -> None:
         record["migration"]["replacement"] = "PNT.Hex.bklnwBounds"
         inventory.require_migrations([record])
 
+    def test_finished_classification_requires_existing_evidence_path(self) -> None:
+        record = {
+            "kind": "dependency-interface",
+            "migration": {
+                "status": "accepted-unchanged",
+                "note": "ported",
+                "evidence": ["conformance/HexIntervalMathlib/Missing.lean"],
+            },
+        }
+        with self.assertRaisesRegex(inventory.InventoryError, "evidence path"):
+            inventory.require_migrations([record])
+
     def test_dependency_surface_must_match_all_six_interfaces(self) -> None:
         imports = [
             {"module": module, "path": "X.lean", "line": index + 1}