interval: run search on reified goals

HexInterval/SPEC/hex-interval.md

@@ -1385,16 +1385,18 @@ ambiguous package matches remain hard registry errors. All accepted hypotheses
 narrowing the same version-zero node remain in an ordered seed recipe; later
 hypotheses cannot overwrite an earlier proof dependency, while facts about
 other recognized expressions may append a suffix after the target graph. The
-exponential tactic currently requires only the target-reachable operation and
-node prefixes, and the target fact, to match its fixed semantic/proof fixture.
+fixed-fixture exponential tactic currently requires only the target-reachable
+operation and node prefixes, and the target fact, to match its semantic/proof
+fixture.
 Extra supported, duplicate, unsupported-real, and non-real hypotheses therefore
 do not disable an otherwise applicable proof; later operation packages may
 also extend the registry after the target prefix. Removing that last prefix
 comparison requires package-compositional construction of the program
 semantics and generic proof emission for the recorded top/assumption seed
-recipes. `GoalClosure` now supplies those two proof bridges; running compiled
-search on the resulting dynamic checker input remains the next frontend
-experiment rather than an assumed capability.
+recipes. `GoalClosure` supplies those two proof bridges, and the dynamic
+exponential vertical below now starts compiled search on the resulting checker
+input. A general policy-driven target-closure loop remains future work rather
+than an assumed capability.
 
 The first package-composed semantics experiment removes a second fixed-graph
 assumption. An operation-meaning package supplies an opaque operation signature
@@ -1448,15 +1450,34 @@ actual reified goal. One variant closes from the live exponential replay; a
 second consumes a caller hypothesis through the ordered seed path. Neither
 uses `native_decide`.
 
-This experiment still uses the exponential canary's fixed compiled search
-trace when the target is not already a caller fact, so it presently requires
-the reified graph to be exactly that two-node target graph. The next step is to
-start the generic session from the reifier's `CheckerInput`, select the target
-node in that session, and feed its dynamically quoted trace to
-`ProofFrontend`. That removes the last exact-graph check and lets supported
-hypotheses append unrelated nodes without changing proof production. Key-
-resolved semantic model selection must land before operation packages may be
-reordered; array position is not a permanent package identity.
+This experiment removes the exponential canary's fixed compiled trace.
+It starts `PolicySession` from the reifier's actual `CheckerInput`, selects an
+offer anchored at the actual target node, quotes that resulting session, and
+feeds it to `ProofFrontend` with the dynamic base program, facts, and reflexive
+extension proofs. The ordinary tactic theorem now accepts an unrelated
+supported exponential hypothesis which appends two nodes after the target,
+and it proves `0 ≤ exp (exp x)` from a three-node target graph. Neither case
+adds a nested-exponential or extra-hypothesis branch to goal closure, semantic
+model construction, dependency assembly, or proof replay.
+
+This vertical deliberately selects one target rule whose first improvement is
+version one. General search must instead let the policy run until target
+subsumption, contradiction, or a resource limit and then select the resolved
+target version from the retained proof table. The current 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
+reifier admits up to sixteen nodes and expression depth eight. Thus the single
+unrelated supported hypothesis above fits, while two such hypotheses or a
+sufficiently deep nested target fail at session preflight before search. The
+current canary helper also collapses that resource stop, absence of a matching
+offer, rule failure, and proof-registry failure into one generic diagnostic.
+Aligning the two envelopes and preserving the typed stop reason in tactic
+diagnostics remain future frontend work; neither limitation is a theorem-
+production assumption.
 
 The fixed canary also requires a live session with no dropped work and an exact
 proof history of one instance, one equality, three fact events, and the

conformance/HexIntervalMathlib/ExpSignConformance.lean

@@ -161,12 +161,15 @@ def offer? (session : PolicySession.Session Bound)
               viewed)
   | .resource _ _ | .contradiction _ | .invalidSession _ => none
 
-def invokesExp (offer : Propagator.Policy.OfferView) : Bool :=
+def invokesExpAt (target : NodeId) (offer : Propagator.Policy.OfferView) : Bool :=
   match offer.key with
   | .invoke invocation =>
-      invocation.rule == expRuleKey && invocation.anchor == node 1
+      invocation.rule == expRuleKey && invocation.anchor == target
   | _ => false
 
+def invokesExp (offer : Propagator.Policy.OfferView) : Bool :=
+  invokesExpAt (node 1) offer
+
 def contracted? : Option (PolicySession.Session Bound) := do
   let .ok session := start | none
   let (_, selection, viewed) ← offer? session invokesExp
@@ -195,6 +198,20 @@ def fixture? : Option Fixture := do
   | .ok registry => some { session, registry }
   | .error _ => none
 
+def fixtureInput? (input : CheckerInput Bound) : Option Fixture := do
+  let .ok session := PolicySession.Session.start factDomain
+      input.baseProgram packages input.initialFacts limits
+    | none
+  let (_, selection, viewed) ← offer? session (invokesExpAt input.target.node)
+  let session ←
+    match viewed.choose (.select selection) with
+    | .rule _ observation next =>
+        if observation.outcome == .success then some next else none
+    | _ => none
+  match ProofRegistry.build session.registry proofPackages with
+  | .ok registry => some { session, registry }
+  | .error _ => none
+
 #guard
   fixture?.any fun fixture =>
     fixture.registry.emit.find? expFactSchema.key == some ``expFactSchema
@@ -352,13 +369,49 @@ private meta def emitEvidence : MetaM Expr := do
     | throwError "interval_exp: target fact was not emitted"
   pure proof
 
+private def inputContext (result : GoalFrontend.Result Bound)
+    (base : GoalClosure.BaseProof) : ProofFrontend.Context Bound Name :=
+  { encoder := boundEncoder
+    resolveSchema := pure
+    semantics := mkConst ``semantics
+    domain := mkConst ``boundSchema
+    laws := mkConst ``laws
+    stableLaw := mkConst ``stableLaw
+    input := base.input
+    assumed := ``seedAssumed
+    baseFacts := result.baseFacts
+    baseFactsTerm := base.facts
+    baseProgram := result.input.baseProgram
+    baseProgramTerm := base.program
+    basePrefix := base.basePrefix
+    baseWithin := base.within
+    initialExtension := base.extension
+    finalPrefix := base.basePrefix
+    sameOperations := base.sameOperations
+    top := boundSchema.top }
+
+private meta def emitInput (result : GoalFrontend.Result Bound)
+    (base : GoalClosure.BaseProof) : MetaM Expr := do
+  let some fixture := fixtureInput? result.input
+    | throwError "interval_exp: dynamic search or proof registry failed"
+  let some trace := Frontend.trace? fixture.session.state.engine fixture.session.arena
+    | throwError "interval_exp: dynamic chronology quotation failed"
+  unless trace.program == result.input.baseProgram do
+    throwError "interval_exp: exponential rule unexpectedly changed the graph"
+  let state ← ProofFrontend.emitTrace (inputContext result base)
+    trace.program trace.events fixture.registry.emit
+  let target : SeenVersion :=
+    { node := result.input.target.node, version := 1 }
+  let some proof :=
+      ProofFrontend.findProof? state.known target result.input.target.fact
+    | throwError "interval_exp: dynamic target fact was not emitted"
+  pure proof
+
 private def expTarget (x : ℝ) : Prop :=
   0 ≤ Real.exp x
 
 private meta def proveModeledExp (target : Expr) : MetaM Expr := do
   let result ← reifyGoal target
-  unless result.input.baseProgram == ExpSign.program do
-    throwError "interval_exp model test: expected the exact target graph"
   let some fallback := GoalClosure.termAt? result.terms { index := 0 }
     | throwError "interval_exp model test: missing source expression"
   if (← observing? <| GoalClosure.proveModel (mkConst ``Real) fallback
@@ -385,10 +438,7 @@ private meta def proveModeledExp (target : Expr) : MetaM Expr := do
         mkAppM ``seedAssumed
           #[base.program, base.facts, mkNatLit index, factTerm, found]
     | none =>
-        if result.baseFacts == ExpSign.baseFacts then
-          emitEvidence
-        else
-          throwError "interval_exp model test: fixed trace has different base facts"
+        emitInput result base
   let proof ←
     mkAppM ``Evidence.proof #[evidence, model.valuation, model.proof, facts]
   unless ← isDefEq (← inferType proof) target do
@@ -425,6 +475,14 @@ info: 'Hex.IntervalMathlib.ExpSignConformance.tacticExpModeledSeed' depends on a
 #guard_msgs in
 #print axioms tacticExpModeledSeed
 
+theorem tacticExpModeledExtra (x y : ℝ) (_hy : 0 ≤ Real.exp y) :
+    0 ≤ Real.exp x := by
+  interval_exp_model
+
+theorem tacticExpModeledNested (x : ℝ) :
+    0 ≤ Real.exp (Real.exp x) := by
+  interval_exp_model
+
 private meta def proveExp (target : Expr) : MetaM Expr := do
   let reified ← reifyGoal target
   unless sameTargetGraph reified.input do

progress/20260811T134139Z.md

@@ -0,0 +1,25 @@
+# Accomplished
+
+- Started exponential search from the goal reifier's actual checker input
+  instead of the fixed two-node fixture.
+- Selected the exponential offer at the actual target node and passed that
+  session's own quoted trace through the generic proof frontend.
+- Added ordinary modeled tactic theorems for a graph extended by an unrelated
+  supported hypothesis and for the distinct three-node goal `exp (exp x)`.
+
+# Current frontier
+
+The arbitrary-function frontend now connects goal recognition, dynamic search,
+package semantics, proof replay, caller assumptions, and final Lean closure for
+several graph shapes. The exponential client deliberately performs one selected
+target contraction.
+
+# Next step
+
+Replace the one-action exponential driver with a generic policy loop that runs
+until target subsumption, contradiction, or a resource limit and then closes
+the resolved target version.
+
+# Blockers
+
+None.

progress/20260811T164326Z.md

@@ -0,0 +1,22 @@
+# Accomplished
+
+- Reconciled dynamic goal execution with the repaired goal-closure,
+  operation-semantics, and arbitrary-function frontend stack.
+- Preserved the policy session's use of the exact reified `CheckerInput`,
+  dynamic trace quotation, package-composed semantic model, and kernel-checked
+  target theorem.
+
+# Current frontier
+
+The exponential canary no longer requires an exact two-node fixture: nested
+and unrelated supported graph nodes can be present while the live policy
+session selects the exact target fact and the frontend reconstructs its proof.
+
+# Next step
+
+Finish builds and checks, push this exact head for review, then reconcile the
+generic policy-run controller and target subsumption layer.
+
+# Blockers
+
+None.

progress/20260811T165931Z.md

@@ -0,0 +1,20 @@
+# Accomplished
+
+- Propagated compile-checked axiom reports for both goal-closure exponential
+  theorems into dynamic goal execution.
+- Preserved the extra-node and nested-goal canaries around the new reports.
+
+# Current frontier
+
+Dynamic search and proof construction are unchanged. Both earlier modeled-goal
+entry points now fail compilation if their axiom dependencies differ from the
+standard `propext`, `Classical.choice`, and `Quot.sound` set.
+
+# Next step
+
+Push this exact head after focused checks, then propagate the same trust canary
+through the policy and branch descendants.
+
+# Blockers
+
+None.

progress/20260812T043304Z.md

@@ -0,0 +1,25 @@
+# Accomplished
+
+- Reconciled the dynamic-goal frontend commit onto current `main` after its
+  former stacked base merged.
+- Preserved the exact reified-input session, dynamic target selection, live
+  quotation, and generic proof-emission feature patch.
+- Documented the tighter exponential engine envelope and its currently generic
+  resource diagnostic alongside the broader goal-reifier envelope.
+
+# Current frontier
+
+The dynamic exponential vertical supports the demonstrated extra-node and
+nested-target canaries, but its session preflight remains limited to five nodes
+and node depth four even though goal reification accepts sixteen nodes and
+expression depth eight.
+
+# Next step
+
+Align frontend and engine resource envelopes, preserve typed stop reasons in
+tactic diagnostics, and replace the one-action canary driver with a generic
+target-closure loop.
+
+# Blockers
+
+None.