interval: replay a live split through exp

HexInterval/Experiment/ExpSign.lean

@@ -23,10 +23,11 @@ namespace Hex.Interval.Experiment.ExpSign
 
 open Propagator PayloadArena
 
-/-- Minimal fact lattice for exponential positivity. -/
+/-- Minimal fact lattice for exponential positivity and source sign splits. -/
 inductive Bound where
   | all
   | nonnegative
+  | negative
   | empty
   deriving DecidableEq, Repr
 
@@ -37,16 +38,20 @@ def meet : Bound → Bound → Bound
   | .all, right => right
   | left, .all => left
   | .nonnegative, .nonnegative => .nonnegative
+  | .negative, .negative => .negative
+  | .nonnegative, .negative | .negative, .nonnegative => .empty
 
 def code : Bound → Nat
   | .all => 0
   | .nonnegative => 1
   | .empty => 2
+  | .negative => 3
 
 def ofCode? : Nat → Option Bound
   | 0 => some .all
   | 1 => some .nonnegative
   | 2 => some .empty
+  | 3 => some .negative
   | _ => none
 
 end Bound

HexInterval/SPEC/hex-interval.md

@@ -1353,7 +1353,7 @@ proof closure still name the canary's fixed base graph, declared base list,
 and target; the goal reifier below begins removing that specialization.
 
 A second live vertical validates this separation with `Real.exp`. Its
-Mathlib-free package uses a distinct three-element fact lattice, contributes
+Mathlib-free package uses a distinct four-element fact lattice, contributes
 one unconditional nonnegativity propagator, and has neither instantiation nor
 equality transport. Its Mathlib companion contributes only real semantics and
 one replay schema. The same policy session, joint package registry,
@@ -1582,14 +1582,24 @@ generic Meta frontend now quotes
 the complete child `CheckerInput`, rejects any mismatch in its program, fact
 array, or target, pins the full child assumption list, and turns the seed into
 exact version-zero `FactProof` records. Its branch entry point then uses the
-unchanged function-independent chronology fold. A live child session and a
-nonempty child event trace remain the next end-to-end branch experiment.
+unchanged function-independent chronology fold.
 The shared `emitSeeded` fold is a low-level Meta helper: its raw proof table
 must already refer to the context's quoted base program and child assumptions.
 The caller-root and branch-root entry points establish that precondition via
 `seedBase` and `seedBranch`; later replay use sites still typecheck every
 stored proof expression and fail closed on a mismatch.
 
+The first live branch canary uses the independent real exponential package.
+It partitions the source fact `.all` into `.nonnegative` and strict
+`.negative`, justified by `0 ≤ x ∨ x < 0`. Each exact child input is paired
+with a `BranchSeed`, starts an actual policy session, runs the exponential
+propagator, and retains one ordinary fact event. `emitBranch` replays both
+nonempty traces, `closeTarget` closes the same exponential target in each
+child context, and `replaySplit` joins them into the caller theorem. The
+assigned tactic term is built from those two live child results. This canary
+does not yet claim that an executable `SplitPlan` constructed the child inputs;
+connecting policy selection to branch creation remains branch-manager work.
+
 Branches may instantiate different auxiliary expressions. Each child replay
 therefore closes its target back to the program snapshot at the split before
 the two results are joined. The package-owned `Extends` theorem and semantic
@@ -1628,10 +1638,13 @@ Several operational choices deliberately remain experimental:
   schema generic, or replace it with a registry-resolved opaque landmark.
 
 These choices may change performance and certificate size, but not the
-coverage-and-two-proofs contract. Acceptance tests for the branch layer must
-include a useful two-sided closure, one contradiction leaf plus one target
-leaf, a nested split, a child-local instantiation, a sibling-reference attack,
-a non-interior repeated split, and fuel exhaustion with no theorem emitted.
+coverage-and-two-proofs contract. The real exponential canary supplies the
+first two-sided live execution and proof join, but exponential nonnegativity
+is unconditional: neither child target proof currently needs its split
+assumption. Remaining acceptance tests include a useful branch-dependent
+two-sided closure, one contradiction leaf plus one target leaf, a nested split,
+a child-local instantiation, a sibling-reference attack, a non-interior
+repeated split, and fuel exhaustion with no theorem emitted.
 
 ### Proof-producing frontend
 

HexIntervalMathlib/Experiment/ExpSign.lean

@@ -28,6 +28,7 @@ open GenericInstanceReconstruction OperationSemantics
 def Contains : Bound → ℝ → Prop
   | .all, _ => True
   | .nonnegative, x => 0 ≤ x
+  | .negative, x => x < 0
   | .empty, _ => False
 
 def sourceModel : OperationSemantics.Model ℝ :=
@@ -73,6 +74,20 @@ def laws : Laws semantics :=
       change Contains fact (valuation left) ↔ Contains fact (valuation right)
       rw [values] }
 
+/-- Coverage theorem for the real zero split used by the live branch canary. -/
+def signSplit : SplitSchema semantics Unit where
+  proveCover := fun _ _ parent _ left right =>
+    if shape : parent = .all ∧ left = .nonnegative ∧ right = .negative then
+      some
+        { proof := by
+            rcases shape with ⟨rfl, rfl, rfl⟩
+            intro valuation _ _
+            change NodeId → ℝ at valuation
+            change (0 : ℝ) ≤ valuation _ ∨ valuation _ < 0
+            exact le_or_gt 0 (valuation _) }
+    else
+      none
+
 theorem expEntails (graph : Program) (assumptions : List (NodeFact Bound))
     (output : NodeId) (instruction : Node) (input : NodeId)
     (found : graph.node? output = some instruction)

conformance/HexIntervalMathlib/ExpSignConformance.lean

@@ -264,6 +264,69 @@ def trace? : Option (Frontend.Trace Bound) := do
             step.event.fact == .nonnegative
       | _ => false
 
+/-! ## Live zero-split child sessions -/
+
+private def branchFact (side : Bound) : NodeFact Bound :=
+  { node := node 0, fact := side }
+
+private def branchFacts (side : Bound) : List (NodeFact Bound) :=
+  branchFact side :: baseFacts
+
+private def branchInitial (side : Bound) : Array Bound := #[side, .all]
+
+private def branchInput (side : Bound) : CheckerInput Bound :=
+  { baseProgram := program
+    initialFacts := branchInitial side
+    target := checkerInput.target }
+
+private def inheritBranch (side : Bound) (observed : NodeId)
+    (different : observed ≠ node 0) (fact : Bound)
+    (found : (branchInput side).initialFacts[observed.index]? = some fact) :
+    Evidence
+      (semantics.Entails program baseFacts { node := observed, fact }) :=
+  { proof := by
+      intro _ _ assumptions
+      cases observed with
+      | mk index =>
+          cases index with
+          | zero => simp [node] at different
+          | succ index =>
+              cases index with
+              | zero =>
+                  simp [branchInput, branchInitial] at found
+                  subst fact
+                  exact assumptions _ (by simp [baseFacts, node])
+              | succ index => simp [branchInput, branchInitial] at found }
+
+private def leftInput : CheckerInput Bound := branchInput .nonnegative
+private def rightInput : CheckerInput Bound := branchInput .negative
+private def leftFacts : List (NodeFact Bound) := branchFacts .nonnegative
+private def rightFacts : List (NodeFact Bound) := branchFacts .negative
+
+private def leftSeed :
+    ProofEmitter.BranchSeed semantics leftInput baseFacts
+      (branchFact .nonnegative) :=
+  ProofEmitter.BranchSeed.make leftInput (branchFact .nonnegative)
+    (by rfl) (by rfl) (inheritBranch .nonnegative)
+
+private def rightSeed :
+    ProofEmitter.BranchSeed semantics rightInput baseFacts
+      (branchFact .negative) :=
+  ProofEmitter.BranchSeed.make rightInput (branchFact .negative)
+    (by rfl) (by rfl) (inheritBranch .negative)
+
+#guard
+  runInput? leftInput |>.any fun fixture =>
+    fixture.reached.seen == ({ node := node 1, version := 1 } : SeenVersion) &&
+      fixture.reached.fact == .nonnegative && fixture.events.size == 1 &&
+      fixture.session.state.engine.facts == #[.nonnegative, .nonnegative]
+
+#guard
+  runInput? rightInput |>.any fun fixture =>
+    fixture.reached.seen == ({ node := node 1, version := 1 } : SeenVersion) &&
+      fixture.reached.fact == .nonnegative && fixture.events.size == 1 &&
+      fixture.session.state.engine.facts == #[.negative, .nonnegative]
+
 /-! ## Operation-composed semantics at an arbitrary graph node -/
 
 private def nestedInstruction : Node :=
@@ -421,6 +484,7 @@ theorem nestedExp (x : ℝ) : 0 ≤ Real.exp (Real.exp x) := by
 private def boundExpr : Bound → Expr
   | .all => mkConst ``Bound.all
   | .nonnegative => mkConst ``Bound.nonnegative
+  | .negative => mkConst ``Bound.negative
   | .empty => mkConst ``Bound.empty
 
 private def boundEncoder : FrontendEncoder.Encoder Bound :=
@@ -496,6 +560,83 @@ private def inputContext (result : GoalFrontend.Result Bound)
     sameOperations := base.sameOperations
     top := boundSchema.top }
 
+private theorem branchWithin (side : Bound) :
+    FactsWithin program (branchFacts side) := by
+  intro fact member
+  simp only [branchFacts, branchFact, baseFacts, List.mem_cons,
+    List.not_mem_nil, or_false] at member
+  rcases member with rfl | rfl | rfl <;> simp [program, node]
+
+private def splitContext (input facts within : Expr)
+    (factValues : List (NodeFact Bound)) : ProofFrontend.Context Bound Name :=
+  { encoder := boundEncoder
+    resolveSchema := pure
+    semantics := mkConst ``semantics
+    domain := mkConst ``boundSchema
+    laws := mkConst ``laws
+    stableLaw := mkConst ``stableLaw
+    input
+    assumed := ``seedAssumed
+    baseFacts := factValues
+    baseFactsTerm := facts
+    baseProgram := program
+    baseProgramTerm := mkConst ``program
+    basePrefix := mkConst ``basePrefix
+    baseWithin := within
+    initialExtension := mkConst ``initialExtension
+    finalPrefix := mkConst ``basePrefix
+    sameOperations := mkConst ``sameOperations
+    top := boundSchema.top }
+
+private def leftContext : ProofFrontend.Context Bound Name :=
+  splitContext (mkConst ``leftInput) (mkConst ``leftFacts)
+    (mkApp (mkConst ``branchWithin) (mkConst ``Bound.nonnegative)) leftFacts
+
+private def rightContext : ProofFrontend.Context Bound Name :=
+  splitContext (mkConst ``rightInput) (mkConst ``rightFacts)
+    (mkApp (mkConst ``branchWithin) (mkConst ``Bound.negative)) rightFacts
+
+private def splitParent : Evidence
+    (semantics.Entails program baseFacts (branchFact .all)) :=
+  ProofEmitter.assumed (by simp [baseFacts, branchFact, node])
+
+private meta def emitChild (context : ProofFrontend.Context Bound Name)
+    (input : CheckerInput Bound) (seed : Expr) (side : Bound) : MetaM Expr := do
+  let some fixture := runInput? input
+    | throwError "interval_exp_split: child search failed"
+  let some trace := Frontend.trace? fixture.session.state.engine fixture.session.arena
+    | throwError "interval_exp_split: child chronology quotation failed"
+  unless trace.program == input.baseProgram do
+    throwError "interval_exp_split: child trace changed the expression graph"
+  let [.rule step] := trace.events
+    | throwError "interval_exp_split: child trace is not exactly one fact rule"
+  unless fixture.reached.seen == ({ node := node 1, version := 1 } : SeenVersion) &&
+      fixture.reached.fact == .nonnegative && fixture.events.size == 1 &&
+      fixture.session.state.engine.facts == #[side, .nonnegative] &&
+      step.entry.replayKey == expFactSchema.key &&
+      step.event.programVersion == 0 && step.event.node == node 1 &&
+      step.event.previous == ({ node := node 1, version := 0 } : SeenVersion) &&
+      step.event.fact == .nonnegative && step.event.version == 1 &&
+      step.assumptions == [branchFact side] && step.previous == .all do
+    throwError "interval_exp_split: child result or quoted rule trace drifted"
+  let state ← ProofFrontend.emitBranch context input seed trace.program
+    trace.events fixture.registry.emit
+  ProofFrontend.closeTarget context state fixture.reached.seen
+    fixture.reached.fact input.target
+
+private meta def emitSplit : MetaM Expr := do
+  let left ← emitChild leftContext leftInput (mkConst ``leftSeed) .nonnegative
+  let right ← emitChild rightContext rightInput (mkConst ``rightSeed) .negative
+  let result ←
+    mkAppM ``ProofEmitter.replaySplit
+      #[mkConst ``signSplit, mkConst ``program, mkConst ``baseFacts,
+        ← boundEncoder.nodeId (node 0), ← boundEncoder.fact .all,
+        mkConst ``Unit.unit, ← boundEncoder.fact .nonnegative,
+        ← boundEncoder.fact .negative,
+        ← boundEncoder.nodeFact checkerInput.target,
+        mkConst ``splitParent, left, right]
+  ProofFrontend.replayResult result
+
 private meta def emitInput (result : GoalFrontend.Result Bound)
     (base : GoalClosure.BaseProof) : MetaM Expr := do
   let some fixture := runInput? result.input
@@ -623,6 +764,61 @@ syntax (name := intervalExpTac) "interval_exp" : tactic
 theorem tacticExp (x : ℝ) : 0 ≤ Real.exp x := by
   interval_exp
 
+private meta def proveSplit (target : Expr) : MetaM Expr := do
+  let context ← getLCtx
+  for declaration in context do
+    unless declaration.isImplementationDetail do
+      let saved ← saveState
+      let candidate? ← observing? <|
+        mkAppM ``expTarget #[mkFVar declaration.fvarId]
+      match candidate? with
+      | some candidate =>
+          if ← isDefEq candidate target then
+            let evidence ← emitSplit
+            let proof ←
+              mkAppM ``closeExp #[mkFVar declaration.fvarId, evidence]
+            unless ← isDefEq (← inferType proof) target do
+              throwError "interval_exp_split: joined proof has the wrong target"
+            return (← instantiateMVars proof)
+          saved.restore
+      | none => saved.restore
+  throwError "interval_exp_split: expected a goal `0 ≤ Real.exp x`"
+
+syntax (name := intervalExpSplitTac) "interval_exp_split" : tactic
+
+@[tactic intervalExpSplitTac] meta def evalIntervalExpSplit : Tactic := fun stx => do
+  match stx with
+  | `(tactic| interval_exp_split) =>
+      let goal ← getMainGoal
+      goal.withContext do
+        let proof ← proveSplit (← instantiateMVars (← goal.getType))
+        goal.assign proof
+      replaceMainGoal []
+  | _ => throwUnsupportedSyntax
+
+/-- Both live children run the arbitrary exponential propagator, replay their
+one-event traces, and close only after the zero split coverage theorem joins
+their target proofs. -/
+theorem tacticExpSplit (x : ℝ) : 0 ≤ Real.exp x := by
+  interval_exp_split
+
+/--
+info: 'Hex.IntervalMathlib.ExpSignConformance.tacticExpSplit' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs in
+#print axioms tacticExpSplit
+
+set_option linter.unusedTactic false in
+example : True := by
+  run_tac
+    if (← observing? <| emitChild leftContext rightInput
+        (mkConst ``rightSeed) .negative).isSome then
+      throwError "interval_exp_split: mismatched child input was accepted"
+    if (← observing? <| emitChild rightContext rightInput
+        (mkConst ``leftSeed) .negative).isSome then
+      throwError "interval_exp_split: mismatched branch seed was accepted"
+  trivial
+
 theorem tacticExpExtra (x y : ℝ) (_hy : 0 ≤ Real.exp y) :
     0 ≤ Real.exp x := by
   interval_exp

progress/20260811T152000Z.md

@@ -0,0 +1,31 @@
+# Accomplished
+
+- Extended the small exponential fact domain with a strict-negative fact and
+  proved its meet semantics over `Real`.
+- Added a real zero-split schema proving that `.all` is covered by
+  `.nonnegative` and `.negative`.
+- Constructed exact left and right child inputs and provenance-safe branch
+  seeds over the same arbitrary-function graph.
+- Started two live policy sessions, ran the exponential propagator once in
+  each child, replayed both nonempty traces through `emitBranch`, and joined
+  the child target proofs through `replaySplit`.
+- Added an ordinary tactic theorem whose assigned term is built from those two
+  live child results; no native evaluation participates in the proof.
+- Rebuilt the proof-emitter, sine tactic, and exponential conformance targets
+  successfully.
+
+# Current frontier
+
+The proof side now covers a complete two-child branch-and-propagate cycle.
+Child creation is still driven directly by the conformance fixture rather than
+by an accepted runtime `SplitPlan`.
+
+# Next step
+
+Add the branch manager transition which turns a validated policy split into
+the two exact child inputs, accounts branch resources, and refuses to join
+until every child is closed or proved contradictory.
+
+# Blockers
+
+None.

progress/20260811T152500Z.md

@@ -0,0 +1,19 @@
+# Accomplished
+
+- Clarified the live exponential split canary's exact strength after review.
+- Restored a useful branch-dependent two-sided closure to the remaining
+  acceptance tests.
+
+# Current frontier
+
+The canary executes and proves both branches, but exponential nonnegativity is
+unconditional, so its child proofs do not yet depend on their split assumptions.
+
+# Next step
+
+Connect the accepted runtime split plan to exact child construction, then add
+a function or target whose two child proofs genuinely use different sides.
+
+# Blockers
+
+None.