test(interval): exercise nested branch scheduling

HexInterval/SPEC/hex-interval.md

@@ -1711,6 +1711,18 @@ runs the arbitrary exponential propagator in each, and retains two target
 leaves. Separate guards show that one global step leaves both children pending,
 and that zero split or one-leaf budgets retain an explicitly blocked root.
 
+A second Mathlib-free runtime canary now makes the scheduling abstraction
+observable on live work. Its root splits one source; the side-aware policy
+fork sends only the left child to split a second source, while the right child
+immediately runs the arbitrary exponential propagator. After the nested split,
+the depth-first frontier is `[left-left, left-right, right]` and the
+breadth-first frontier is `[right, left-left, left-right]`; both complete to
+the same five-node retained tree. This catches an ignored `Side` argument and
+an accidental exchange of the scheduler's old and fresh queues. The second
+source is deliberately irrelevant to the exponential target, so this is a
+scheduling and accounting canary, not the still-required useful nested
+subdivision benchmark.
+
 This runtime tree contains no proof evidence. The separate generic
 `BranchProof` frontend now folds a settled retained tree bottom-up. It first
 binds every leaf and split result back to its exact scope, base program, and

conformance/HexInterval/NestedBranchConformance.lean

@@ -0,0 +1,164 @@
+/-
+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 HexInterval.Experiment.BranchTree
+import HexInterval.Experiment.ExpSign
+
+/-!
+# Nested branch scheduling conformance
+
+This Mathlib-free canary builds a live two-level split tree.  The left child
+splits a second source while the right child closes immediately, so the child
+policy fork is genuinely side-sensitive and depth-first and breadth-first
+frontiers differ on live pending work.
+-/
+
+namespace Hex.Interval.NestedBranchConformance
+
+open Experiment
+open Propagator PolicySession SemanticReplay TargetRun BranchStart BranchTree
+open ExpSign
+
+private def program : Program :=
+  { operations
+    nodes := #[sourceInstruction, sourceInstruction, expInstruction] }
+
+private def target : NodeFact Bound :=
+  { node := node 2, fact := .nonnegative }
+
+private def input : CheckerInput Bound :=
+  { baseProgram := program
+    initialFacts := #[.all, .all, .all]
+    target }
+
+private inductive Route where
+  | root
+  | splitLeft
+  | close
+  deriving DecidableEq, Repr
+
+private def splitAt (wanted : NodeId) (view : Policy.View Bound) :
+    Option Policy.OfferView :=
+  view.offers.toList.find? fun offer =>
+    match offer.key with
+    | .invoke invocation =>
+        invocation.rule == splitRuleKey && invocation.anchor == wanted
+    | .split _ seen _ _ => seen.node == wanted
+    | _ => false
+
+private def expAt (wanted : NodeId) (view : Policy.View Bound) :
+    Option Policy.OfferView :=
+  view.offers.toList.find? fun offer =>
+    match offer.key with
+    | .invoke invocation =>
+        invocation.rule == expRuleKey && invocation.anchor == wanted
+    | _ => false
+
+private def controller : Controller Bound Route :=
+  { update := fun state _ => state
+    choose := fun state view =>
+      let selected :=
+        match state with
+        | .root => splitAt (node 0) view
+        | .splitLeft => splitAt (node 1) view
+        | .close => expAt (node 2) view
+      match selected with
+      | some offer => .select offer state
+      | none => .stop state }
+
+private def fork : Route -> Side -> Route
+  | .root, .left => .splitLeft
+  | .root, .right => .close
+  | .splitLeft, _ => .close
+  | .close, _ => .close
+
+private def splitter : Splitter Bound :=
+  { split := fun graph splitNode instruction parent point =>
+      if graph.node? splitNode == some instruction &&
+          instruction.domain == real && parent == .all && point == 0 then
+        some (.nonnegative, .negative)
+      else
+        none }
+
+private def resources : BranchTree.Limits :=
+  { branch := { maxDepth := 3, maxScopes := 5 }
+    maxSteps := 5
+    maxSplits := 2
+    maxLeaves := 3
+    leafFuel := limits.policy.maxDecisions }
+
+private def config (order : Order) : Config Bound Route :=
+  { factDomain
+    packages := splitPackages
+    sessionLimits := limits
+    controller
+    splitter
+    forkPolicy := fork
+    order
+    limits := resources }
+
+private def run? (order : Order) (fuel : Nat) : Option (State Bound Route) := do
+  let .ok state := BranchTree.start (config order) { index := 0 } input .root
+    | none
+  let .ok state := BranchTree.runFrom (config order) fuel state | none
+  some state
+
+private def leafReached? (entry : Node Bound Route) : Bool :=
+  match entry with
+  | .leaf source (.result result) =>
+      source.input.target == target &&
+        match result.stop with
+        | .target reached => reached.seen.node == target.node &&
+            reached.fact == .nonnegative
+        | _ => false
+  | _ => false
+
+#guard fork .root .left == .splitLeft
+#guard fork .root .right == .close
+
+#guard
+  (run? .depthFirst 2).any fun state =>
+    state.steps == 2 && state.splits == 2 && state.leaves == 3 &&
+      state.frontier == [{ index := 3 }, { index := 4 }, { index := 2 }]
+
+#guard
+  (run? .breadthFirst 2).any fun state =>
+    state.steps == 2 && state.splits == 2 && state.leaves == 3 &&
+      state.frontier == [{ index := 2 }, { index := 3 }, { index := 4 }]
+
+#guard
+  (run? .depthFirst 5).any fun state =>
+    state.settled && state.steps == 5 && state.splits == 2 &&
+      state.leaves == 3 && state.nodes.size == 5 &&
+      match state.nodes[0]?, state.nodes[1]?, state.nodes[2]?,
+          state.nodes[3]?, state.nodes[4]? with
+      | some (BranchTree.Node.split root _ rootChildren left right),
+          some (BranchTree.Node.split nested _ nestedChildren nestedLeft nestedRight),
+          some rightLeaf, some nestedLeftLeaf, some nestedRightLeaf =>
+          root.policyState == .root && left.index == 1 && right.index == 2 &&
+            rootChildren.leftScope.index == 1 &&
+            rootChildren.rightScope.index == 2 &&
+            rootChildren.left.initialFacts == #[.nonnegative, .all, .all] &&
+            rootChildren.right.initialFacts == #[.negative, .all, .all] &&
+            nested.policyState == .splitLeft &&
+            nestedLeft.index == 3 && nestedRight.index == 4 &&
+            nestedChildren.leftScope.index == 3 &&
+            nestedChildren.rightScope.index == 4 &&
+            nestedChildren.left.initialFacts ==
+              #[.nonnegative, .nonnegative, .all] &&
+            nestedChildren.right.initialFacts ==
+              #[.nonnegative, .negative, .all] &&
+            leafReached? rightLeaf && leafReached? nestedLeftLeaf &&
+            leafReached? nestedRightLeaf
+      | _, _, _, _, _ => false
+
+#guard
+  (run? .breadthFirst 5).any fun state =>
+    state.settled && state.steps == 5 && state.splits == 2 &&
+      state.leaves == 3 && state.nodes.size == 5 &&
+      state.nodes.toList.countP leafReached? == 3
+
+end Hex.Interval.NestedBranchConformance

lakefile.lean

@@ -402,7 +402,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, `HexInterval.SinTenIntervalConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.ReluConformance, `HexIntervalMathlib.RefuteConformance, `HexIntervalMathlib.PntLogTableConformance, `HexIntervalMathlib.PntNestedLogConformance, `HexIntervalMathlib.PntExpTailConformance, `HexIntervalMathlib.SinTenConformance, `HexIntervalMathlib.SinTenIntervalConformance, `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.NestedBranchConformance, `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, `HexInterval.SinTenIntervalConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.ReluConformance, `HexIntervalMathlib.RefuteConformance, `HexIntervalMathlib.PntLogTableConformance, `HexIntervalMathlib.PntNestedLogConformance, `HexIntervalMathlib.PntExpTailConformance, `HexIntervalMathlib.SinTenConformance, `HexIntervalMathlib.SinTenIntervalConformance, `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

progress/20260811T174943Z.md

@@ -0,0 +1,27 @@
+# Accomplished
+
+- Added a Mathlib-free live two-level branch tree whose left child performs a
+  second split and whose right child immediately runs the exponential
+  propagator.
+- Made the child policy fork depend on `Side`, so exchanging left and right is
+  observable in the retained tree.
+- Checked the exact live depth-first and breadth-first frontiers after the
+  nested split, and checked that both orders settle to three target leaves.
+- Documented that this second split is intentionally a scheduling canary, not
+  yet a useful nested subdivision benchmark.
+
+# Current frontier
+
+Live scheduling now exercises both delivered frontier orders and a
+side-sensitive child policy. The nested split does not affect the target, so
+proof-tree recursion and search usefulness are still separate canaries.
+
+# Next step
+
+Introduce the first actual interval fact representation with open, closed,
+and unbounded endpoints. Reuse the same nested tree with a target whose child
+proofs genuinely improve because of subdivision.
+
+# Blockers
+
+None.

progress/20260814T194607Z.md

@@ -0,0 +1,34 @@
+# PR #9226 local reconciliation
+
+## Accomplished
+
+- Replayed only the nested live-branch scheduling canary onto exact merged
+  #9225 main `54b82bee520e74eeab2e15d5fb44a57f82aa969c`.
+- Preserved all current branch-proof, PNT-log, Machin, and endpoint-sine
+  registrations while adding only `HexInterval.NestedBranchConformance` to the
+  conformance target.
+- Audited that the live two-step frontier makes both `schedule rest fresh`
+  ordering and the `Side` argument to `forkPolicy` observable: depth-first and
+  breadth-first retain distinct exact frontiers, while either side-insensitive
+  route breaks the pinned split, leaf, and settled-tree accounting.
+- Checked the exact retained node identities, child scopes, inherited fact
+  arrays, three target leaves, and the SPEC's honest statement that the second
+  split is target-irrelevant.
+- Recomputed the proof-only Lake exemption for exact resolved blob
+  `d3be6e3f3c99f2bbc3685500563a49f90059d5c1`.
+- Built the focused nested-branch and inherited interval targets and passed the
+  static, trust-surface, freshness, PNT-inventory, diff, and banned-term checks.
+
+## Current frontier
+
+- The feature is prepared as a clean local commit on merged #9225 and remains
+  intentionally unpushed while the exp-tail PR advances `main`.
+
+## Next step
+
+- Rebase this prepared feature once onto the final post-exp-tail `main`, refresh
+  only exact freshness metadata if required, then run final review and CI.
+
+## Blockers
+
+- None.

progress/20260814T200753Z.md

@@ -0,0 +1,28 @@
+# PR #9226 final reconciliation
+
+## Accomplished
+
+- Rebased the audited nested-branch scheduling canary onto exact post-#9261
+  main `37bda079c4c9974da49c9e8a8559a66d2e671b45`.
+- Preserved the complete PNT log-table, nested-log, and exponential-tail
+  experiments and conformance registrations while adding only the nested-branch
+  conformance target.
+- Refreshed the narrow proof-only Lake exemption to exact resolved blob
+  `a869c195af5b211b96e848d4f11754abb64ebcc8`.
+- Rebuilt the nested-branch and inherited branch-proof, ReLU, PNT, and sine
+  targets successfully and reran all focused static, trust, freshness,
+  inventory, diff, and banned-term checks.
+
+## Current frontier
+
+- The exact reconciled candidate is ready to push for final independent review
+  and exact-head CI.
+
+## Next step
+
+- Push and retarget PR #9226 to `main`, then require fresh Opus approval and
+  exact-head CI success before marking it merge-ready.
+
+## Blockers
+
+- None.

scripts/bench/proof_only_runtime_exemptions.json

@@ -185,6 +185,12 @@
     "current_blob": "2943018771d8ab5c7c256f28ce299320c7a646e0",
     "reason": "Additionally registers the Mathlib-free pinned exponential-tail chronology experiment, its proof-only real-semantics companion, and conformance module; the factorization service target and executable dependency graph are unchanged."
   },
+  {
+    "path": "lakefile.lean",
+    "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
+    "current_blob": "a869c195af5b211b96e848d4f11754abb64ebcc8",
+    "reason": "Additionally registers the Mathlib-free HexInterval nested-branch conformance module only; the factorization service target and executable dependency graph are unchanged."
+  },
   {
     "path": "HexBerlekamp/FactorTacticTests.lean",
     "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",