interval: close stronger target facts in the kernel

HexInterval/Experiment/ProofEmitter.lean

@@ -414,6 +414,26 @@ def replayTransport {Fact : Type} {semantics : Semantics Fact}
       else
         none
 
+/-- Close a requested fact from a stronger established fact at the same node.
+The independent fact-domain theorem must prove that intersecting `actual` with
+`requested` leaves `actual` unchanged.  Runtime target detection is not used
+as evidence. -/
+def closeFact {Fact : Type} {semantics : Semantics Fact}
+    (domain : FactDomainSchema semantics) (program : Program)
+    (base : List (NodeFact Fact)) (node : NodeId) (actual requested : Fact)
+    (actualSound :
+      Evidence
+        (semantics.Entails program base { node, fact := actual })) :
+    Option
+      (Evidence
+        (semantics.Entails program base { node, fact := requested })) := do
+  let meet <- domain.proveMeet program node actual requested actual
+  pure
+    { proof := by
+        intro valuation model baseHolds
+        have established := actualSound.proof valuation model baseHolds
+        exact ((meet.proof valuation model).mp established).2 }
+
 /-- Project a proposition from any successfully replayed proof object. -/
 theorem evidenceOfReplay {P : Prop} (result : Option (Evidence P))
     (success : result.isSome) : P :=

HexInterval/Experiment/ProofFrontend.lean

@@ -142,6 +142,24 @@ def replayResult (result : Expr) : MetaM Expr := do
   let success ← mkAppM ``Eq.refl #[mkConst ``Bool.true]
   mkAppM ``replayGet #[result, success]
 
+/-- Emit a kernel-checked subsumption step from one exact retained fact version
+to the caller's requested fact. -/
+def closeTarget [BEq Fact] (context : Context Fact Handle)
+    (state : State Fact) (seen : SeenVersion) (actual : Fact)
+    (target : NodeFact Fact) : MetaM Expr := do
+  unless seen.node == target.node do
+    throwError "interval frontend: retained result is for the wrong target node"
+  let some established := findFact? state.known seen actual
+    | throwError "interval frontend: retained target version has not been proved"
+  let nodeTerm ← context.encoder.nodeId target.node
+  let actualTerm ← context.encoder.fact actual
+  let requestedTerm ← context.encoder.fact target.fact
+  let result ←
+    mkAppM ``ProofEmitter.closeFact
+      #[context.domain, state.program, context.baseFactsTerm, nodeTerm,
+        actualTerm, requestedTerm, established.proof]
+  replayResult result
+
 /-- Seed caller-owned version-zero facts by exact positions in the base list. -/
 def seedBase (context : Context Fact Handle) (program : Expr) (basePrefix : Expr) :
     MetaM (List (FactProof Fact)) := do

HexInterval/SPEC/hex-interval.md

@@ -1472,19 +1472,24 @@ packages and function names do not occur in the driver.
 Target subsumption is a runtime stopping test: narrowing the current fact by
 the requested fact must report no change. The result records the exact current
 fact and version, but neither that test nor the controller is proof evidence.
-Proof emission must still resolve the retained version and replay an independent
-fact-domain subsumption theorem. The exponential conformance policy simply
-selects the first offer. On `exp (exp x)` it therefore improves the inner and
-outer nodes in two separate steps, stops at the requested outer bound, and
-feeds both chronological events to the unchanged generic proof frontend.
-
-The current conformance closes only when the retained target fact is exactly
-the requested fact. Closing from a strictly stronger retained fact is the next
-proof-frontend connection. The driver returns split plans but does not yet
-create or join proof branches. The operation registry also remains the fixed
-source/exponential pair. Key-resolved semantic model selection must land before
-operation packages may be reordered; array position is not a permanent package
-identity.
+`ProofFrontend.closeTarget` resolves that exact retained proof and applies the
+transparent `ProofEmitter.closeFact` combinator. The combinator independently
+asks `FactDomainSchema.proveMeet` to prove that intersecting the established
+fact with the requested fact leaves the established fact unchanged; only that
+kernel theorem supplies the requested conclusion. A conformance theorem closes
+`.all` from a strictly stronger `.nonnegative` fact through the transparent
+`closeFact` combinator. The live frontend canaries exercise `closeTarget` with
+an exact retained target fact; an end-to-end strict-subsumption frontend
+canary remains useful coverage rather than a delivered claim.
+
+The exponential conformance policy simply selects the first offer. On
+`exp (exp x)` it therefore improves the inner and outer nodes in two separate
+steps, stops at the requested outer bound, and feeds both chronological events
+to the unchanged generic proof frontend. The driver returns split plans but
+does not yet create or join proof branches. The operation registry also remains
+the fixed source/exponential pair. Key-resolved semantic model selection must
+land before operation packages may be reordered; array position is not a
+permanent package identity.
 
 The dynamic path is still bounded by the exponential package's engine envelope,
 which permits at most five nodes and node depth four, even though the goal

conformance/HexIntervalMathlib/ExpSignConformance.lean

@@ -277,6 +277,40 @@ private def nestedInput : CheckerInput Bound :=
     initialFacts := #[.all, .all, .all]
     target := { node := node 2, fact := .nonnegative } }
 
+private def nonnegativeEvidence :
+    Evidence
+      (semantics.Entails program baseFacts
+        { node := node 1, fact := .nonnegative }) :=
+  { proof :=
+      expEntails program baseFacts (node 1) expInstruction (node 0)
+        (by rfl) (by rfl) (by rfl) }
+
+private def weakerTarget? :
+    Option
+      (Evidence
+        (semantics.Entails program baseFacts
+          { node := node 1, fact := .all })) :=
+  ProofEmitter.closeFact boundSchema program baseFacts (node 1)
+    .nonnegative .all nonnegativeEvidence
+
+/-- A strictly stronger installed fact closes a weaker requested target
+through the fact-domain intersection theorem, not the runtime target test. -/
+theorem closesWeaker :
+    semantics.Entails program baseFacts { node := node 1, fact := .all } :=
+  (replayGet weakerTarget? (by rfl)).proof
+
+private def topEvidence :
+    Evidence
+      (semantics.Entails program baseFacts
+        { node := node 1, fact := .all }) := by
+  simpa [boundSchema, expInstruction] using
+    (ProofEmitter.topFact boundSchema program baseFacts (node 1)
+      expInstruction (by rfl))
+
+#guard
+  (ProofEmitter.closeFact boundSchema program baseFacts (node 1)
+    .all .nonnegative topEvidence).isNone
+
 #guard
   runInput? nestedInput |>.any fun fixture =>
     fixture.reached.seen == ({ node := node 2, version := 1 } : SeenVersion) &&
@@ -472,10 +506,8 @@ private meta def emitInput (result : GoalFrontend.Result Bound)
     throwError "interval_exp: exponential rule unexpectedly changed the graph"
   let state ← ProofFrontend.emitTrace (inputContext result base)
     trace.program trace.events fixture.registry.emit
-  let some proof :=
-      ProofFrontend.findProof? state.known fixture.reached.seen result.input.target.fact
-    | throwError "interval_exp: dynamic target fact was not emitted"
-  pure proof
+  ProofFrontend.closeTarget (inputContext result base) state fixture.reached.seen
+    fixture.reached.fact result.input.target
 
 private def expTarget (x : ℝ) : Prop :=
   0 ≤ Real.exp x

progress/20260811T141300Z.md

@@ -0,0 +1,28 @@
+# Kernel target closure
+
+## Accomplished
+
+- Added a transparent generic combinator which closes a requested fact from a
+  stronger established fact only when the fact-domain schema proves the exact
+  intersection theorem.
+- Added a proof-frontend bridge which resolves the runner's exact retained
+  fact version and emits that kernel-checked subsumption step.
+- Routed dynamic exponential target closure through the new bridge.
+- Added an ordinary theorem closing `.all` from strictly stronger
+  `.nonnegative` evidence and a negative guard rejecting the converse.
+
+## Current frontier
+
+Target-directed propagation and final fact subsumption are both generic and
+proof-producing. Prepared split plans are returned but no branch theorem owns
+or joins their child proofs yet.
+
+## Next step
+
+Specify and prototype branch ownership for subdivision, including interval
+coverage, child resource scopes, contradiction leaves, and kernel-checked
+joining of successful children.
+
+## Blockers
+
+None.

progress/20260811T142200Z.md

@@ -0,0 +1,20 @@
+# Accomplished
+
+- Narrowed the target-closure SPEC claim to match the implemented conformance:
+  strict subsumption is exercised directly through the transparent proof
+  combinator, while the live frontend currently closes an exact target fact.
+
+# Current frontier
+
+The generic frontend path and the independently checked stronger-to-weaker
+proof combinator are both present, but their conjunction still needs one
+strict-subsumption frontend canary.
+
+# Next step
+
+Add wrong-node, wrong-version, wrong-fact, and strict-subsumption frontend
+coverage as the target-proof table is generalized.
+
+# Blockers
+
+None.

progress/20260811T164557Z.md

@@ -0,0 +1,23 @@
+# Accomplished
+
+- Reconciled generic target closure with the repaired dynamic policy runner and
+  proof frontend stack.
+- Preserved exact node/version lookup and kernel-checked fact subsumption, so a
+  stronger established fact may close a weaker requested target without
+  treating runtime reachability as evidence.
+
+# Current frontier
+
+Single-branch execution can now stop on a reached target and close that target
+through a package-independent fact-domain proof. The live canaries currently
+exercise exact target facts; strict end-to-end subsumption remains useful
+additional coverage.
+
+# Next step
+
+Finish builds and checks, push the exact head for review, then reconcile the
+proof-side split/join boundary and authenticated branch seeding.
+
+# Blockers
+
+None.

progress/20260811T170057Z.md

@@ -0,0 +1,17 @@
+# Accomplished
+
+- Propagated both compile-checked modeled-goal axiom reports through generic
+  target closure.
+
+# Current frontier
+
+Target subsumption and proof closure are unchanged; the earlier generated
+theorems retain explicit standard-axiom regression checks.
+
+# Next step
+
+Push after the focused build, then continue through split and branch layers.
+
+# Blockers
+
+None.

progress/20260814T100139Z.md

@@ -0,0 +1,38 @@
+# Interval target-closure restack
+
+## Accomplished
+
+- Restacked the target-closure feature from PR #9215 first onto the reviewed PR
+  #9214 head and then onto exact post-merge `main`
+  `433806f976f5586e6e4c053710e6d5f24314e768`, whose second parent is that
+  reviewed #9214 head and whose tree is identical.
+- Verified that the `ProofEmitter`, `ProofFrontend`, and exponential conformance
+  patches retain the same stable patch identities as the approved source
+  commit.
+- Audited `closeFact`: its result follows only from the exact established proof
+  and the fact-domain `proveMeet` theorem specialized to an unchanged meet.
+- Audited `closeTarget`: it requires the exact retained `(node, version, fact)`
+  proof and fails closed when the node, version, fact, or meet proof differs.
+- Preserved the SPEC distinction between direct strict-subsumption coverage and
+  the current exact-fact live frontend canaries, together with PR #9214's
+  resource-envelope and provenance limitations.
+- Built `HexInterval.Experiment.ProofEmitter`,
+  `HexInterval.Experiment.ProofFrontend`, and
+  `HexIntervalMathlib.ExpSignConformance` successfully (1952 jobs).
+- Passed copyright, dependency-DAG, published-trust-surface, Phase 4,
+  factor-freshness, diff-whitespace, and added-line banned-mechanism checks.
+
+## Current frontier
+
+- The restacked code and documentation are locally verified and ready for an
+  exact-head independent review and CI run.
+
+## Next step
+
+- Push the verified post-merge restack with force-with-lease, obtain a fresh
+  isolated Opus review of the exact head, and monitor its exact GitHub Actions
+  run.
+
+## Blockers
+
+- None.