From 2a0d3e41da980f8cd8a84a992c99f9c0a9fe3757 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 11 Aug 2026 17:24:19 +0000
Subject: [PATCH 1/4] Propagate provenance honesty through branch runtime;
 progress 20260811T171522Z

---
 HexInterval/Experiment/BranchStart.lean       | 211 +++++++++++++++++
 HexInterval/Experiment/ExpSign.lean           |  28 +++
 HexInterval/Experiment/Propagator.lean        |   4 +-
 HexInterval/SPEC/hex-interval.md              |  61 +++--
 HexIntervalMathlib/Experiment/ExpSign.lean    |  11 +
 .../ExpSignConformance.lean                   | 212 ++++++++++++++++--
 lakefile.lean                                 |   1 +
 progress/20260811T153000Z.md                  |  29 +++
 progress/20260811T154328Z.md                  |  30 +++
 progress/20260811T165424Z.md                  |  24 ++
 progress/20260811T170358Z.md                  |  18 ++
 .../bench/proof_only_runtime_exemptions.json  |   6 +
 12 files changed, 603 insertions(+), 32 deletions(-)
 create mode 100644 HexInterval/Experiment/BranchStart.lean
 create mode 100644 progress/20260811T153000Z.md
 create mode 100644 progress/20260811T154328Z.md
 create mode 100644 progress/20260811T165424Z.md
 create mode 100644 progress/20260811T170358Z.md

diff --git a/HexInterval/Experiment/BranchStart.lean b/HexInterval/Experiment/BranchStart.lean
new file mode 100644
index 000000000..70dc32967
--- /dev/null
+++ b/HexInterval/Experiment/BranchStart.lean
@@ -0,0 +1,211 @@
+/-
+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.TargetRun
+public import HexInterval.Experiment.SemanticReplay
+
+@[expose] public section
+
+/-!
+# Checked branch starts
+
+This experiment turns one policy-owned split plan into two exact child
+`CheckerInput`s.  It is representation- and function-independent: the fact
+domain checks strict narrowing, while a registered splitter interprets the
+domain-specific cut.
+
+The transition is search infrastructure, not proof evidence.  The proof
+frontend must still seed inherited parent evidence, add exactly one child
+assumption, and replay a package-owned coverage theorem before joining the
+children.
+-/
+
+namespace Hex.Interval.Experiment.BranchStart
+
+open Propagator PolicySession SemanticReplay TargetRun
+
+/-- Tree-wide branch resources, separate from each child session's own limits. -/
+structure Limits where
+  maxDepth : Nat
+  maxScopes : Nat
+  deriving DecidableEq, Repr
+
+/-- Monotone identities and resource use owned by one branch tree. -/
+structure State where
+  createdScopes : Nat
+  nextScope : Nat
+  deriving DecidableEq, Repr
+
+namespace State
+
+/-- Account for the already-existing root scope. -/
+def start (root : Propagator.Policy.ScopeId) : State :=
+  { createdScopes := 1, nextScope := root.index + 1 }
+
+end State
+
+/-- A domain package translates the executable cut into two proposed child
+facts.  The generic manager independently checks that each proposal is the
+exact result of a strict narrowing step. -/
+structure Splitter (Fact : Type) where
+  split : Program -> NodeId -> Node -> Fact -> Dyadic -> Option (Fact × Fact)
+
+/-- Exact parent and child snapshots prepared by one accepted split. -/
+structure Children (Fact : Type) where
+  plan : Propagator.Policy.SplitPlan Fact
+  depth : Nat
+  parent : CheckerInput Fact
+  leftScope : Propagator.Policy.ScopeId
+  left : CheckerInput Fact
+  rightScope : Propagator.Policy.ScopeId
+  right : CheckerInput Fact
+
+/-- Fail-closed reasons for refusing to create child sessions. -/
+inductive Error where
+  | inactive
+  | incomplete
+  | contradictory
+  | wrongScope
+  | wrongOrigin
+  | staleProgram
+  | staleOrigin
+  | unknownNode
+  | staleFact
+  | staleVersion
+  | unknownTarget
+  | unsupportedCut
+  | duplicateChild
+  | leftNotStrict
+  | rightNotStrict
+  | depthLimit
+  | scopeLimit
+  deriving DecidableEq, Repr
+
+def strictChild [DecidableEq Fact] (domain : FactDomain Fact) (instruction : Node)
+    (parent child : Fact) : Bool :=
+  match domain.narrow instruction.domain parent child with
+  | .improved installed => installed == child
+  | .noChange | .contradiction _ | .malformed _ | .resourceLimit _ => false
+
+/-- Validate one selected plan and allocate two fresh child scopes.
+
+The child snapshots start from the parent's current program and complete fact
+array, replacing only the split node.  Proof production must authenticate all
+unchanged entries as inherited parent facts; this function never promotes
+them to caller assumptions. -/
+def prepare [DecidableEq Fact] (limits : Limits) (state : State) (depth : Nat)
+    (session : Session Fact) (plan : Propagator.Policy.SplitPlan Fact)
+    (target : NodeFact Fact) (splitter : Splitter Fact) :
+    Except Error (State × Children Fact) := do
+  if !session.live then throw .inactive
+  if session.droppedWork || session.state.incomplete then throw .incomplete
+  if session.state.engine.contradictory then throw .contradictory
+  if plan.scope != session.state.scope then throw .wrongScope
+  if plan.source != Propagator.Policy.invocationOfAction plan.scope plan.origin then
+    throw .wrongOrigin
+  let engine := session.state.engine
+  if plan.origin.programVersion != engine.programVersion then throw .staleProgram
+  if !engine.actionFresh plan.origin then throw .staleOrigin
+  let instruction <-
+    match engine.program.node? plan.node with
+    | some instruction => pure instruction
+    | none => throw .unknownNode
+  let current <-
+    match engine.facts[plan.node.index]? with
+    | some fact => pure fact
+    | none => throw .unknownNode
+  if current != plan.fact then throw .staleFact
+  let version <-
+    match engine.versions[plan.node.index]? with
+    | some version => pure version
+    | none => throw .unknownNode
+  if version != plan.version then throw .staleVersion
+  if (engine.program.node? target.node).isNone then throw .unknownTarget
+  let (leftFact, rightFact) <-
+    match splitter.split engine.program plan.node instruction plan.fact plan.point with
+    | some children => pure children
+    | none => throw .unsupportedCut
+  if leftFact == rightFact then throw .duplicateChild
+  if !strictChild engine.factDomain instruction plan.fact leftFact then
+    throw .leftNotStrict
+  if !strictChild engine.factDomain instruction plan.fact rightFact then
+    throw .rightNotStrict
+  let childDepth := depth + 1
+  if childDepth > limits.maxDepth then throw .depthLimit
+  if state.createdScopes + 2 > limits.maxScopes then throw .scopeLimit
+  let leftScope : Propagator.Policy.ScopeId := { index := state.nextScope }
+  let rightScope : Propagator.Policy.ScopeId := { index := state.nextScope + 1 }
+  let parent : CheckerInput Fact :=
+    { baseProgram := engine.program, initialFacts := engine.facts, target }
+  let left : CheckerInput Fact :=
+    { parent with initialFacts := engine.facts.set! plan.node.index leftFact }
+  let right : CheckerInput Fact :=
+    { parent with initialFacts := engine.facts.set! plan.node.index rightFact }
+  let next : State :=
+    { createdScopes := state.createdScopes + 2, nextScope := state.nextScope + 2 }
+  pure (next,
+    { plan, depth := childDepth, parent, leftScope, left, rightScope, right })
+
+/-- Runtime classification of one child result.  `contradiction` is a search
+status only; a proof-producing join still needs a checked refutation schema. -/
+inductive LeafStatus (Fact : Type)
+  | target (reached : TargetRun.Reached Fact)
+  | contradiction
+  | unfinished
+  | wrongInput
+
+def sameInput [DecidableEq Fact] (scope : Propagator.Policy.ScopeId)
+    (input : CheckerInput Fact)
+    (result : TargetRun.Result Fact PolicyState) : Bool :=
+  result.session.state.scope == scope &&
+    result.session.state.engine.baseProgram == input.baseProgram &&
+    result.session.state.engine.initialFacts == input.initialFacts
+
+/-- Classify a child only after binding its run back to the exact prepared
+input.  Target closure is rechecked against the retained current fact and
+version. -/
+def status [DecidableEq Fact] (domain : FactDomain Fact)
+    (scope : Propagator.Policy.ScopeId) (input : CheckerInput Fact)
+    (result : TargetRun.Result Fact PolicyState) :
+    LeafStatus Fact :=
+  if !sameInput scope input result then .wrongInput
+  else
+    let engine := result.session.state.engine
+    match result.stop with
+    | .target reached =>
+        if reached.seen.node != input.target.node then .unfinished
+        else
+          match engine.program.node? reached.seen.node,
+              engine.facts[reached.seen.node.index]?,
+              engine.versions[reached.seen.node.index]? with
+          | some instruction, some fact, some version =>
+              if fact != reached.fact || version != reached.seen.version then .unfinished
+              else
+                match domain.narrow instruction.domain fact input.target.fact with
+                | .noChange => .target reached
+                | .improved _ | .contradiction _ | .malformed _ | .resourceLimit _ =>
+                    .unfinished
+          | _, _, _ => .unfinished
+    | .contradiction =>
+        if engine.contradictory then .contradiction else .unfinished
+    | _ => .unfinished
+
+/-- Refuse the ordinary two-proof join unless both exact child runs reached
+their requested targets.  Contradictory children deliberately do not pass:
+they need proof-producing refutation before generic elimination is sound. -/
+def closedTargets? [DecidableEq Fact] (domain : FactDomain Fact)
+    (children : Children Fact)
+    (left : TargetRun.Result Fact LeftState)
+    (right : TargetRun.Result Fact RightState) :
+    Option (TargetRun.Reached Fact × TargetRun.Reached Fact) :=
+  match status domain children.leftScope children.left left,
+      status domain children.rightScope children.right right with
+  | .target left, .target right => some (left, right)
+  | _, _ => none
+
+end Hex.Interval.Experiment.BranchStart
diff --git a/HexInterval/Experiment/ExpSign.lean b/HexInterval/Experiment/ExpSign.lean
index 56ded04db..595821f1f 100644
--- a/HexInterval/Experiment/ExpSign.lean
+++ b/HexInterval/Experiment/ExpSign.lean
@@ -69,6 +69,7 @@ def real : DomainId := { index := 0 }
 def sourceKey : OpKey := { name := "exp-sign.source" }
 def expKey : OpKey := { name := "exp-sign.exp" }
 def expRuleKey : RuleKey := { name := "exp-sign.exp.nonnegative" }
+def splitRuleKey : RuleKey := { name := "exp-sign.source.split-zero" }
 
 def sourceOperation : Operation :=
   { key := sourceKey, inputs := [], output := real }
@@ -98,6 +99,15 @@ def expRule : Registration :=
     watches := [.argument 0]
     writes := [.result] }
 
+/-- The source package may suggest zero as a domain-owned landmark.  It does
+not construct either branch. -/
+def splitRule : Registration :=
+  { key := splitRuleKey
+    head := sourceKey
+    kind := .split
+    watches := [.result]
+    writes := [] }
+
 def factFormat : ReplayFormat :=
   { role := .fact
     schema := 1
@@ -121,6 +131,14 @@ def expPlan (request : RuleRequest Bound) : Plan Bound :=
              body := [Bound.nonnegative.code] }] }
   | _, _ => { outcome := .failed 1, drafts := [] }
 
+def splitInvoke (request : RuleRequest Bound) : Outcome Bound :=
+  match request.inputs, request.writes with
+  | [input], [] =>
+      .success []
+        [.split { node := input.node, point := 0, reason := .smallLandmark }]
+        { visitedEntries := 1 }
+  | _, _ => .failed 2
+
 def sourcePackage : Package Bound :=
   { Cache := Unit
     cache := ()
@@ -133,8 +151,18 @@ def expPackage : Package Bound :=
     operations := #[expOperation]
     handlers := #[Handler.statelessPlanned expRule expPlan #[factFormat]] }
 
+def splitPackage : Package Bound :=
+  { Cache := Unit
+    cache := ()
+    requiredOperations := #[sourceOperation]
+    handlers := #[Handler.statelessDroppingDrafts splitRule splitInvoke] }
+
 def packages : Array (Package Bound) := #[sourcePackage, expPackage]
 
+/-- Search configuration which additionally admits the optional zero landmark. -/
+def splitPackages : Array (Package Bound) :=
+  #[sourcePackage, expPackage, splitPackage]
+
 def engineLimits : Propagator.Limits :=
   { maxOperations := 3
     maxNodes := 5
diff --git a/HexInterval/Experiment/Propagator.lean b/HexInterval/Experiment/Propagator.lean
index f173246c7..50f58c6bc 100644
--- a/HexInterval/Experiment/Propagator.lean
+++ b/HexInterval/Experiment/Propagator.lean
@@ -848,8 +848,8 @@ inductive SplitReason where
   | custom (code : Nat)
   deriving DecidableEq, Repr
 
-/-- A proof-split suggestion.  The engine alone creates complementary child
-scopes; the rule supplies only a node, cut, and reason. -/
+/-- A proof-split suggestion.  The rule supplies only a node, cut, and reason;
+a checked branch manager creates complementary child scopes and facts. -/
 structure SplitRequest where
   node : NodeId
   point : Dyadic
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 49dd7d052..9c41a066a 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -1485,11 +1485,12 @@ 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.
+to the unchanged generic proof frontend. The target driver returns split plans
+without itself owning a search tree; the separate checked branch-start layer
+now creates exact child inputs. The operation table 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
@@ -1596,9 +1597,30 @@ 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.
+assigned tactic term is built from those two live child results.
+
+The corresponding executable source package now contributes a zero-landmark
+split rule. The generic `BranchStart.prepare` transition consumes the selected
+`SplitPlan` only after checking its exact scope and reconstructing its source
+key from the supplied origin. That origin must also pass the retained engine's
+full action-freshness check: its application, registration, watched versions,
+write authority, program-sensitive version, and structural matcher provenance
+must still match engine-owned state. The transition separately checks the
+program version, node fact, and fact version for precise diagnostics. A
+domain-supplied
+`Splitter` interprets the dyadic cut; the manager independently requires both
+returned facts to be distinct, exact `.improved` results of `FactDomain.narrow`.
+It replaces only the selected slot in the parent's complete current fact
+array, preserves the target and current program, assigns two fresh child scope
+identities, and charges separate tree depth and total-scope limits. The live
+canary checks that these prepared inputs are exactly the two proof-side inputs
+above, then starts both child sessions under the allocated scopes.
+
+The executable split package currently emits no replayable fact, instance, or
+equality event, but it still occupies a package-ownership position. Its proof
+registry therefore contains an explicit empty package at that same position.
+Conformance checks both directions: split-enabled registry assembly succeeds
+with the placeholder and rejects the shorter ordinary proof-package array.
 
 Branches may instantiate different auxiliary expressions. Each child replay
 therefore closes its target back to the program snapshot at the split before
@@ -1617,14 +1639,21 @@ search diagnostics but cannot participate in a completed join. An unexplored,
 fuel-limited, resource-limited, incomplete, or merely saturated child likewise
 does not close the parent target.
 
-The first branch manager should retain a tree whose internal node records the
-validated plan and checked child facts, and whose leaves retain either a target
-proof, a checked contradiction, or an explicit unfinished result. It may emit
-a theorem only when every coverage child is closed. For best-bound mode,
-unfinished leaves contribute their inherited parent fact to the global hull;
-they never inherit a tighter sibling fact. Split depth, total created scopes,
-live leaves, and total branch decisions receive separate limits in addition to
-the per-session engine and payload limits.
+The first branch-start layer also rebinds each completed child result to the
+exact prepared base program and initial fact array, then rechecks the retained
+target fact and version. Its ordinary two-target closure gate rejects a stopped,
+saturated, fuel-limited, malformed, or wrong-input child. It classifies a
+runtime contradiction separately but deliberately refuses to treat that flag
+as proof closure; the refutation schema described above must land first.
+
+The remaining tree manager should retain internal nodes recording validated
+plans and checked child facts, and leaves retaining either a target proof, a
+checked contradiction, or an explicit unfinished result. It may emit a theorem
+only when every coverage child is closed. For best-bound mode, unfinished
+leaves contribute their inherited parent fact to the global hull; they never
+inherit a tighter sibling fact. Live-leaf and total branch-decision limits
+remain to be added beside the delivered split-depth and total-created-scope
+limits and the per-session engine and payload limits.
 
 Several operational choices deliberately remain experimental:
 
diff --git a/HexIntervalMathlib/Experiment/ExpSign.lean b/HexIntervalMathlib/Experiment/ExpSign.lean
index 7c7e3fc4b..9453b7646 100644
--- a/HexIntervalMathlib/Experiment/ExpSign.lean
+++ b/HexIntervalMathlib/Experiment/ExpSign.lean
@@ -167,9 +167,20 @@ def expProof : ProofRegistry.Package semantics Lean.Name :=
   { semantic := { factSchemas := #[expFactSchema] }
     emit := expEmit }
 
+/-- Proof-side placeholder for the executable split package, which owns no
+replay formats.  Retaining its package position keeps registry ownership
+aligned even before a split-coverage schema is added. -/
+def splitProof : ProofRegistry.Package semantics Lean.Name :=
+  { semantic := { factSchemas := #[] }
+    emit := { schemas := [] } }
+
 def proofPackages : Array (ProofRegistry.Package semantics Lean.Name) :=
   #[sourceProof, expProof]
 
+/-- Proof packages aligned with the split-enabled executable registry. -/
+def splitProofPackages : Array (ProofRegistry.Package semantics Lean.Name) :=
+  #[sourceProof, expProof, splitProof]
+
 def semanticPackages : Array (SemanticReplay.Package semantics) :=
   proofPackages.map (fun package => package.semantic)
 
diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean
index ea81d8d07..78c34ad50 100644
--- a/conformance/HexIntervalMathlib/ExpSignConformance.lean
+++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean
@@ -9,6 +9,7 @@ import HexInterval.Experiment.GoalFrontend
 import HexInterval.Experiment.GoalClosure
 import HexInterval.Experiment.ProofFrontend
 import HexInterval.Experiment.TargetRun
+import HexInterval.Experiment.BranchStart
 import Mathlib.Lean.Elab.Tactic.Meta
 
 /-!
@@ -27,7 +28,7 @@ open Lean Elab Tactic Meta
 open Hex.Interval.Experiment
 open Propagator PolicySession SemanticReplay ChronologicalReplay ProofEmitter
 open Frontend FrontendEncoder ProofFrontend ProofRegistry GoalFrontend ExpSign
-open GoalClosure
+open GoalClosure BranchStart
 
 /-! ## Extensible goal reification -/
 
@@ -228,16 +229,24 @@ structure RunFixture extends Fixture where
   reached : TargetRun.Reached Bound
   events : Array (TargetRun.Event Bound)
 
-def runRaw? (input : CheckerInput Bound) (controller : TargetRun.Controller Bound Unit)
-    (fuel : Nat) : Option (TargetRun.Result Bound Unit) := do
+def runWith? (runtimePackages : Array (Package Bound))
+    (input : CheckerInput Bound) (controller : TargetRun.Controller Bound Unit)
+    (fuel : Nat) (scope : Propagator.Policy.ScopeId := { index := 0 }) :
+    Option (TargetRun.Result Bound Unit) := do
   let .ok session := PolicySession.Session.start factDomain
-      input.baseProgram packages input.initialFacts limits
+      input.baseProgram runtimePackages input.initialFacts limits scope
     | none
   some (TargetRun.drive factDomain input.target.node input.target.fact controller
     fuel session ())
 
-def runInput? (input : CheckerInput Bound) : Option RunFixture := do
-  let result <- runRaw? input firstOffer limits.policy.maxDecisions
+def runRaw? (input : CheckerInput Bound) (controller : TargetRun.Controller Bound Unit)
+    (fuel : Nat) (scope : Propagator.Policy.ScopeId := { index := 0 }) :
+    Option (TargetRun.Result Bound Unit) :=
+  runWith? packages input controller fuel scope
+
+def runInput? (input : CheckerInput Bound)
+    (scope : Propagator.Policy.ScopeId := { index := 0 }) : Option RunFixture := do
+  let result <- runRaw? input firstOffer limits.policy.maxDecisions scope
   let .target reached := result.stop | none
   match ProofRegistry.build result.session.registry proofPackages with
   | .ok registry =>
@@ -266,6 +275,60 @@ def trace? : Option (Frontend.Trace Bound) := do
 
 /-! ## Live zero-split child sessions -/
 
+private def splitOffer? (view : Propagator.Policy.View Bound) :
+    Option Propagator.Policy.OfferView :=
+  view.offers.toList.find? fun offer =>
+    match offer.key with
+    | .invoke invocation => invocation.rule == splitRuleKey
+    | .split _ _ _ _ => true
+    | _ => false
+
+private def splitPolicy : TargetRun.Controller Bound Unit :=
+  { update := fun state _ => state
+    choose := fun state view =>
+      match splitOffer? view with
+      | some offer => .select offer state
+      | none => .stop state }
+
+private def signSplitter : BranchStart.Splitter Bound :=
+  { split := fun graph target instruction parent point =>
+      if graph.node? target == some instruction && instruction.domain == real &&
+          parent == .all && point == 0 then
+        some (.nonnegative, .negative)
+      else
+        none }
+
+private def branchLimits : BranchStart.Limits :=
+  { maxDepth := 4, maxScopes := 8 }
+
+private def prepared? : Option (ULift.{1, 0} (BranchStart.Children Bound)) :=
+  match runWith? splitPackages checkerInput splitPolicy limits.policy.maxDecisions with
+  | none => none
+  | some result =>
+      match result.stop with
+      | .split plan =>
+          match BranchStart.prepare branchLimits
+              (BranchStart.State.start { index := 0 }) 0 result.session plan
+              checkerInput.target signSplitter with
+          | .ok (_, children) => some (ULift.up children)
+          | .error _ => none
+      | _ => none
+
+private def splitRun? : Option (TargetRun.Result Bound Unit) :=
+  runWith? splitPackages checkerInput splitPolicy limits.policy.maxDecisions
+
+#guard
+  splitRun?.any fun result =>
+    match ProofRegistry.build result.session.registry splitProofPackages with
+    | .ok _ => true
+    | .error _ => false
+
+#guard
+  splitRun?.any fun result =>
+    match ProofRegistry.build result.session.registry proofPackages with
+    | .error (.semantic (.packageCount 3 2)) => true
+    | _ => false
+
 private def branchFact (side : Bound) : NodeFact Bound :=
   { node := node 0, fact := side }
 
@@ -300,6 +363,8 @@ private def inheritBranch (side : Bound) (observed : NodeId)
 
 private def leftInput : CheckerInput Bound := branchInput .nonnegative
 private def rightInput : CheckerInput Bound := branchInput .negative
+private def leftScope : Propagator.Policy.ScopeId := { index := 1 }
+private def rightScope : Propagator.Policy.ScopeId := { index := 2 }
 private def leftFacts : List (NodeFact Bound) := branchFacts .nonnegative
 private def rightFacts : List (NodeFact Bound) := branchFacts .negative
 
@@ -316,17 +381,133 @@ private def rightSeed :
     (by rfl) (by rfl) (inheritBranch .negative)
 
 #guard
-  runInput? leftInput |>.any fun fixture =>
+  prepared?.any fun lifted =>
+    let children := lifted.down
+    children.depth == 1 &&
+      children.parent.baseProgram == checkerInput.baseProgram &&
+      children.parent.initialFacts == checkerInput.initialFacts &&
+      children.parent.target == checkerInput.target &&
+      children.leftScope == leftScope &&
+      children.left.baseProgram == leftInput.baseProgram &&
+      children.left.initialFacts == leftInput.initialFacts &&
+      children.left.target == leftInput.target &&
+      children.rightScope == rightScope &&
+      children.right.baseProgram == rightInput.baseProgram &&
+      children.right.initialFacts == rightInput.initialFacts &&
+      children.right.target == rightInput.target &&
+      children.plan.point == 0 && children.plan.fact == .all
+
+#guard
+  runInput? leftInput leftScope |>.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 =>
+  runInput? rightInput rightScope |>.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]
 
+private def closedChildren? : Option
+    (ULift.{1, 0} (TargetRun.Reached Bound × TargetRun.Reached Bound)) :=
+  match prepared? with
+  | none => none
+  | some lifted =>
+      let children := lifted.down
+      match runRaw? children.left firstOffer limits.policy.maxDecisions
+          children.leftScope,
+        runRaw? children.right firstOffer limits.policy.maxDecisions
+          children.rightScope with
+      | some left, some right =>
+          (BranchStart.closedTargets? factDomain children left right).map ULift.up
+      | _, _ => none
+
+#guard closedChildren?.isSome
+
+#guard
+  prepared?.any fun lifted =>
+    let children := lifted.down
+    match runRaw? children.left stopPolicy limits.policy.maxDecisions
+        children.leftScope,
+      runRaw? children.right firstOffer limits.policy.maxDecisions
+        children.rightScope with
+    | some left, some right =>
+        (BranchStart.closedTargets? factDomain children left right).isNone
+    | _, _ => false
+
+#guard
+  prepared?.any fun lifted =>
+    let children := lifted.down
+    match runRaw? children.left firstOffer limits.policy.maxDecisions { index := 99 },
+      runRaw? children.right firstOffer limits.policy.maxDecisions children.rightScope with
+    | some left, some right =>
+        (BranchStart.closedTargets? factDomain children left right).isNone
+    | _, _ => false
+
+#guard
+  match runWith? splitPackages checkerInput splitPolicy limits.policy.maxDecisions with
+  | some result =>
+      match result.stop with
+      | .split plan =>
+          match BranchStart.prepare
+              { branchLimits with maxDepth := 0 }
+              (BranchStart.State.start { index := 0 }) 0 result.session plan
+              checkerInput.target signSplitter with
+          | .error .depthLimit => true
+          | _ => false
+      | _ => false
+  | none => false
+
+#guard
+  match splitRun? with
+  | some result =>
+      match result.stop with
+      | .split plan =>
+          let staleOrigin :=
+            { plan.origin with
+              application := { index := result.session.state.engine.applications.size } }
+          let stalePlan :=
+            { plan with
+              origin := staleOrigin
+              source := Propagator.Policy.invocationOfAction plan.scope staleOrigin }
+          match BranchStart.prepare branchLimits
+              (BranchStart.State.start { index := 0 }) 0 result.session stalePlan
+              checkerInput.target signSplitter with
+          | .error .staleOrigin => true
+          | _ => false
+      | _ => false
+  | none => false
+
+#guard
+  match runWith? splitPackages checkerInput splitPolicy limits.policy.maxDecisions with
+  | some result =>
+      match result.stop with
+      | .split plan =>
+          match BranchStart.prepare branchLimits
+              (BranchStart.State.start { index := 0 }) 0 result.session
+              { plan with version := plan.version + 1 }
+              checkerInput.target signSplitter with
+          | .error .staleVersion => true
+          | _ => false
+      | _ => false
+  | none => false
+
+#guard
+  match runWith? splitPackages checkerInput splitPolicy limits.policy.maxDecisions with
+  | some result =>
+      match result.stop with
+      | .split plan =>
+          let duplicate : BranchStart.Splitter Bound :=
+            { split := fun _ _ _ _ _ => some (.nonnegative, .nonnegative) }
+          match BranchStart.prepare branchLimits
+              (BranchStart.State.start { index := 0 }) 0 result.session plan
+              checkerInput.target duplicate with
+          | .error .duplicateChild => true
+          | _ => false
+      | _ => false
+  | none => false
+
 /-! ## Operation-composed semantics at an arbitrary graph node -/
 
 private def nestedInstruction : Node :=
@@ -601,8 +782,9 @@ private def splitParent : Evidence
   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
+    (input : CheckerInput Bound) (scope : Propagator.Policy.ScopeId)
+    (seed : Expr) (side : Bound) : MetaM Expr := do
+  let some fixture := runInput? input scope
     | 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"
@@ -625,8 +807,10 @@ private meta def emitChild (context : ProofFrontend.Context Bound Name)
     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 left ← emitChild leftContext leftInput leftScope
+    (mkConst ``leftSeed) .nonnegative
+  let right ← emitChild rightContext rightInput rightScope
+    (mkConst ``rightSeed) .negative
   let result ←
     mkAppM ``ProofEmitter.replaySplit
       #[mkConst ``signSplit, mkConst ``program, mkConst ``baseFacts,
@@ -812,10 +996,10 @@ set_option linter.unusedTactic false in
 example : True := by
   run_tac
     if (← observing? <| emitChild leftContext rightInput
-        (mkConst ``rightSeed) .negative).isSome then
+        rightScope (mkConst ``rightSeed) .negative).isSome then
       throwError "interval_exp_split: mismatched child input was accepted"
     if (← observing? <| emitChild rightContext rightInput
-        (mkConst ``leftSeed) .negative).isSome then
+        rightScope (mkConst ``leftSeed) .negative).isSome then
       throwError "interval_exp_split: mismatched branch seed was accepted"
   trivial
 
diff --git a/lakefile.lean b/lakefile.lean
index 4c861820d..e0b65d612 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -307,6 +307,7 @@ lean_lib HexIntervalExperiment where
     `HexInterval.Experiment.PayloadSession,
     `HexInterval.Experiment.PolicySession,
     `HexInterval.Experiment.TargetRun,
+    `HexInterval.Experiment.BranchStart,
     `HexInterval.Experiment.SemanticReplay,
     `HexInterval.Experiment.ChronologicalReplay,
     `HexInterval.Experiment.GenericInstanceReconstruction,
diff --git a/progress/20260811T153000Z.md b/progress/20260811T153000Z.md
new file mode 100644
index 000000000..8d4adb097
--- /dev/null
+++ b/progress/20260811T153000Z.md
@@ -0,0 +1,29 @@
+# Accomplished
+
+- Added a function-independent branch-start transition which validates a
+  selected split against the exact policy session.
+- Added domain-supplied child construction with independent strict-narrowing
+  checks, fresh scope allocation, and tree depth/scope accounting.
+- Added exact child-result rebinding and a two-target closure gate which
+  rejects unfinished, wrong-input, and merely runtime-contradictory leaves.
+- Added an optional exponential zero-landmark rule and showed that its accepted
+  `SplitPlan` produces the exact two child inputs consumed by the live proof
+  canary.
+- Ran both child sessions under their allocated scopes and added stale-version,
+  duplicate-child, depth-limit, and unfinished-child rejection tests.
+
+# Current frontier
+
+An accepted runtime plan now reaches the already-delivered live child replay
+and proof join without function cases in the manager. Runtime contradiction is
+still only a search status, not a proof of `False`.
+
+# Next step
+
+Add a package-owned refutation schema for an established bottom fact, then add
+a useful branch-dependent closure whose child proofs genuinely consume their
+different split assumptions.
+
+# Blockers
+
+None.
diff --git a/progress/20260811T154328Z.md b/progress/20260811T154328Z.md
new file mode 100644
index 000000000..1d0411d22
--- /dev/null
+++ b/progress/20260811T154328Z.md
@@ -0,0 +1,30 @@
+# Accomplished
+
+- Required every accepted branch plan origin to pass the retained engine's
+  full `actionFresh` provenance check after the existing source-key and program
+  checks.
+- Added an explicit empty proof package for the split-only runtime package, so
+  split-enabled executable and proof registries retain exact package ownership
+  alignment.
+- Added conformance guards which isolate rejection of a self-consistent forged
+  origin, successful three-package proof-registry assembly, and rejection of
+  the old shorter proof-package array.
+- Updated the branch-design SPEC to state both invariants and their current
+  conformance coverage.
+
+# Current frontier
+
+Validated split plans now remain tied to retained engine provenance, and a
+split-enabled parent session can assemble its proof registry before child
+execution. The split package still emits no replay event and therefore needs
+only the explicit empty proof-side package.
+
+# Next step
+
+Add the branch-dependent two-sided operation canary without adding function
+knowledge to `BranchStart`, then replace the empty split proof package when a
+runtime split-coverage event is introduced.
+
+# Blockers
+
+None.
diff --git a/progress/20260811T165424Z.md b/progress/20260811T165424Z.md
new file mode 100644
index 000000000..087f07bc0
--- /dev/null
+++ b/progress/20260811T165424Z.md
@@ -0,0 +1,24 @@
+# Accomplished
+
+- Reconciled authenticated branch-start runtime with the repaired live
+  split/join stack.
+- Preserved retained-engine action freshness, split-package/proof-package
+  alignment, exact child scope/input construction, and refusal of forged or
+  stale plans.
+- Updated the proof-only Lake exemption to the exact reconciled branch-start
+  registration blob while retaining current factorization exemptions.
+
+# Current frontier
+
+A prepared split can now be authenticated against the live engine and turned
+into two exact child roots. The implementation still runs one split directly;
+it does not yet retain a general tree of unfinished leaves.
+
+# Next step
+
+Finish builds and checks, push the exact head for review, then connect the
+already-reconciled refutation and useful branch-dependent ReLU verticals.
+
+# Blockers
+
+None.
diff --git a/progress/20260811T170358Z.md b/progress/20260811T170358Z.md
new file mode 100644
index 000000000..2e42c11fb
--- /dev/null
+++ b/progress/20260811T170358Z.md
@@ -0,0 +1,18 @@
+# Accomplished
+
+- Propagated both compile-checked modeled-goal axiom reports through the
+  authenticated branch-start runtime.
+
+# Current frontier
+
+Split-plan authentication and child construction are unchanged; inherited
+goal-proof canaries retain explicit standard-axiom checks.
+
+# Next step
+
+Push after the focused build, then continue through refutation and mixed-branch
+closure.
+
+# Blockers
+
+None.
diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json
index 9b69ae11a..5cb57c7b3 100644
--- a/scripts/bench/proof_only_runtime_exemptions.json
+++ b/scripts/bench/proof_only_runtime_exemptions.json
@@ -131,6 +131,12 @@
     "current_blob": "4c861820dbf8db07758455a01f04156f59ad2439",
     "reason": "Additionally registers the Mathlib-free interval target-run driver only; the factorization service target and executable dependency graph are unchanged."
   },
+  {
+    "path": "lakefile.lean",
+    "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
+    "current_blob": "e0b65d612b56feae1fc9f239addea5d045266526",
+    "reason": "Additionally registers the Mathlib-free checked interval branch-start transition only; the factorization service target and executable dependency graph are unchanged."
+  },
   {
     "path": "HexBerlekamp/FactorTacticTests.lean",
     "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",

From 1bbdeb72c1a107da30986a78270da43157fcf8f1 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Wed, 12 Aug 2026 05:45:22 +0000
Subject: [PATCH 2/4] interval: authenticate retained split plans

Seal branch tree accounting and add negative provenance guards. Record the completed repair in progress/20260812T054503Z.md.
---
 HexInterval/Experiment/BranchStart.lean       |  55 +++++--
 HexInterval/SPEC/hex-interval.md              |  34 +++--
 .../ExpSignConformance.lean                   | 142 ++++++++++++++----
 progress/20260812T054503Z.md                  |  37 +++++
 4 files changed, 216 insertions(+), 52 deletions(-)
 create mode 100644 progress/20260812T054503Z.md

diff --git a/HexInterval/Experiment/BranchStart.lean b/HexInterval/Experiment/BranchStart.lean
index 70dc32967..71b407095 100644
--- a/HexInterval/Experiment/BranchStart.lean
+++ b/HexInterval/Experiment/BranchStart.lean
@@ -35,17 +35,25 @@ structure Limits where
   maxScopes : Nat
   deriving DecidableEq, Repr
 
-/-- Monotone identities and resource use owned by one branch tree. -/
+/-- Monotone identities, active-scope depths, and resource use owned by one
+branch tree.  The private constructor prevents callers from choosing counters
+or registering a scope at an invented depth. -/
 structure State where
+  private mk ::
   createdScopes : Nat
   nextScope : Nat
-  deriving DecidableEq, Repr
+  private scopeDepths : List (Propagator.Policy.ScopeId × Nat)
+
+private def makeState (createdScopes nextScope : Nat)
+    (scopeDepths : List (Propagator.Policy.ScopeId × Nat)) : State :=
+  { createdScopes, nextScope, scopeDepths }
 
 namespace State
 
-/-- Account for the already-existing root scope. -/
-def start (root : Propagator.Policy.ScopeId) : State :=
-  { createdScopes := 1, nextScope := root.index + 1 }
+/-- Account for the already-existing root scope of this exact engine-owned
+session.  The sealed result can advance only through `prepare`. -/
+opaque start (session : Session Fact) : State :=
+  makeState 1 (session.state.scope.index + 1) [(session.state.scope, 0)]
 
 end State
 
@@ -71,6 +79,11 @@ inductive Error where
   | incomplete
   | contradictory
   | wrongScope
+  | wrongState
+  | endpointLimit
+  | unknownSuggestion
+  | wrongSuggestion
+  | wrongSuggestionVersion
   | wrongOrigin
   | staleProgram
   | staleOrigin
@@ -92,13 +105,14 @@ def strictChild [DecidableEq Fact] (domain : FactDomain Fact) (instruction : Nod
   | .improved installed => installed == child
   | .noChange | .contradiction _ | .malformed _ | .resourceLimit _ => false
 
-/-- Validate one selected plan and allocate two fresh child scopes.
+/-- Validate one retained split plan and allocate two fresh child scopes.
 
 The child snapshots start from the parent's current program and complete fact
 array, replacing only the split node.  Proof production must authenticate all
 unchanged entries as inherited parent facts; this function never promotes
-them to caller assumptions. -/
-def prepare [DecidableEq Fact] (limits : Limits) (state : State) (depth : Nat)
+them to caller assumptions.  The state supplies the parent depth; a caller
+cannot reset that depth independently of its registered scope. -/
+opaque prepare [DecidableEq Fact] (limits : Limits) (state : State)
     (session : Session Fact) (plan : Propagator.Policy.SplitPlan Fact)
     (target : NodeFact Fact) (splitter : Splitter Fact) :
     Except Error (State × Children Fact) := do
@@ -106,9 +120,27 @@ def prepare [DecidableEq Fact] (limits : Limits) (state : State) (depth : Nat)
   if session.droppedWork || session.state.incomplete then throw .incomplete
   if session.state.engine.contradictory then throw .contradictory
   if plan.scope != session.state.scope then throw .wrongScope
+  let depth <-
+    match state.scopeDepths.find? (fun entry => entry.1 == session.state.scope) with
+    | some entry => pure entry.2
+    | none => throw .wrongState
+  let engine := session.state.engine
+  if !(EndpointCost.ofDyadic plan.point).allowed engine.limits.splitEndpointLimit then
+    throw .endpointLimit
   if plan.source != Propagator.Policy.invocationOfAction plan.scope plan.origin then
     throw .wrongOrigin
-  let engine := session.state.engine
+  let retained <-
+    match engine.suggestions[plan.suggestion.index]? with
+    | some retained => pure retained
+    | none => throw .unknownSuggestion
+  if retained.action != plan.origin then throw .wrongOrigin
+  match retained.suggestion with
+  | .split request =>
+      if request.node != plan.node || request.point != plan.point ||
+          request.reason != plan.reason then
+        throw .wrongSuggestion
+  | .retry _ | .instantiate _ => throw .wrongSuggestion
+  if retained.splitVersion != some plan.version then throw .wrongSuggestionVersion
   if plan.origin.programVersion != engine.programVersion then throw .staleProgram
   if !engine.actionFresh plan.origin then throw .staleOrigin
   let instruction <-
@@ -146,8 +178,9 @@ def prepare [DecidableEq Fact] (limits : Limits) (state : State) (depth : Nat)
     { parent with initialFacts := engine.facts.set! plan.node.index leftFact }
   let right : CheckerInput Fact :=
     { parent with initialFacts := engine.facts.set! plan.node.index rightFact }
-  let next : State :=
-    { createdScopes := state.createdScopes + 2, nextScope := state.nextScope + 2 }
+  let remaining := state.scopeDepths.filter (fun entry => entry.1 != session.state.scope)
+  let next := makeState (state.createdScopes + 2) (state.nextScope + 2)
+    ((leftScope, childDepth) :: (rightScope, childDepth) :: remaining)
   pure (next,
     { plan, depth := childDepth, parent, leftScope, left, rightScope, right })
 
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 9c41a066a..45e1644d7 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -1600,21 +1600,33 @@ child context, and `replaySplit` joins them into the caller theorem. The
 assigned tactic term is built from those two live child results.
 
 The corresponding executable source package now contributes a zero-landmark
-split rule. The generic `BranchStart.prepare` transition consumes the selected
-`SplitPlan` only after checking its exact scope and reconstructing its source
-key from the supplied origin. That origin must also pass the retained engine's
-full action-freshness check: its application, registration, watched versions,
-write authority, program-sensitive version, and structural matcher provenance
-must still match engine-owned state. The transition separately checks the
-program version, node fact, and fact version for precise diagnostics. A
-domain-supplied
+split rule. The generic `BranchStart.prepare` transition does not trust the
+public fields of the `SplitPlan` it receives. It resolves the plan's exact
+retained suggestion identifier and requires that record to contain a split
+with the same complete action (including its request serial), node, dyadic
+cut, reason, and proposal-time fact version. It also checks the exact scope
+and reconstructs the source key from that action. The action must pass the
+retained engine's full freshness check: its application, registration,
+watched versions, write authority, program-sensitive version, and structural
+matcher provenance must still match engine-owned state. The transition
+separately checks the current program version, node fact, and fact version for
+precise diagnostics, and repeats the configured endpoint-cost preflight at
+this boundary so a directly constructed plan cannot bypass it. This
+authenticates the plan against retained engine data; the search controller
+still owns the policy decision that selected that offer. A domain-supplied
 `Splitter` interprets the dyadic cut; the manager independently requires both
 returned facts to be distinct, exact `.improved` results of `FactDomain.narrow`.
 It replaces only the selected slot in the parent's complete current fact
 array, preserves the target and current program, assigns two fresh child scope
-identities, and charges separate tree depth and total-scope limits. The live
-canary checks that these prepared inputs are exactly the two proof-side inputs
-above, then starts both child sessions under the allocated scopes.
+identities, and charges separate tree depth and total-scope limits. Branch-tree
+state has a private constructor: its root is derived from an engine-owned
+session, and only `prepare` can remove an active parent scope, register its two
+children at the next depth, or advance the monotone counters. The live canary
+checks that these prepared inputs are exactly the two proof-side inputs above,
+then starts both child sessions under the allocated scopes. Its Meta tactic is
+still deliberately hard-coded to quote those canary constants rather than the
+runtime `Children` value; dynamically quoting an arbitrary prepared branch is
+a later frontend bridge, not a property established by this experiment.
 
 The executable split package currently emits no replayable fact, instance, or
 equality event, but it still occupies a package-ownership position. Its proof
diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean
index 78c34ad50..b601491ae 100644
--- a/conformance/HexIntervalMathlib/ExpSignConformance.lean
+++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean
@@ -301,22 +301,56 @@ private def signSplitter : BranchStart.Splitter Bound :=
 private def branchLimits : BranchStart.Limits :=
   { maxDepth := 4, maxScopes := 8 }
 
-private def prepared? : Option (ULift.{1, 0} (BranchStart.Children Bound)) :=
+private def preparedResult? : Option
+    (ULift.{1, 0} (BranchStart.State × BranchStart.Children Bound)) :=
   match runWith? splitPackages checkerInput splitPolicy limits.policy.maxDecisions with
   | none => none
   | some result =>
       match result.stop with
       | .split plan =>
           match BranchStart.prepare branchLimits
-              (BranchStart.State.start { index := 0 }) 0 result.session plan
+              (BranchStart.State.start result.session) result.session plan
               checkerInput.target signSplitter with
-          | .ok (_, children) => some (ULift.up children)
+          | .ok prepared => some (ULift.up prepared)
           | .error _ => none
       | _ => none
 
+private def prepared? : Option (ULift.{1, 0} (BranchStart.Children Bound)) :=
+  preparedResult?.map fun lifted => ULift.up lifted.down.2
+
 private def splitRun? : Option (TargetRun.Result Bound Unit) :=
   runWith? splitPackages checkerInput splitPolicy limits.policy.maxDecisions
 
+private def planError? (change : Propagator.Policy.SplitPlan Bound →
+    Propagator.Policy.SplitPlan Bound)
+    (branchBudget : BranchStart.Limits := branchLimits) : Option BranchStart.Error :=
+  match splitRun? with
+  | some result =>
+      match result.stop with
+      | .split plan =>
+          match BranchStart.prepare branchBudget
+              (BranchStart.State.start result.session) result.session (change plan)
+              checkerInput.target signSplitter with
+          | .error error => some error
+          | .ok _ => none
+      | _ => none
+  | none => none
+
+private def unrelatedAction? (result : TargetRun.Result Bound Unit)
+    (plan : Propagator.Policy.SplitPlan Bound) : Option Action := do
+  let engine := result.session.state.engine
+  let index ← (List.range engine.applications.size).find?
+    (fun index => index != plan.origin.application.index)
+  let applicationId : ApplicationId := { index }
+  let application ← engine.applications[index]?
+  let rule ← engine.rules[application.rule.index]?
+  let inputs ← engine.seenVersions? application.watches
+  let views ← engine.factViews? application.watches
+  match engine.issueApplication applicationId application rule inputs views with
+  | .request request _ =>
+      if engine.actionFresh request.action then some request.action else none
+  | _ => none
+
 #guard
   splitRun?.any fun result =>
     match ProofRegistry.build result.session.registry splitProofPackages with
@@ -397,6 +431,11 @@ private def rightSeed :
       children.right.target == rightInput.target &&
       children.plan.point == 0 && children.plan.fact == .all
 
+#guard
+  preparedResult?.any fun lifted =>
+    let state := lifted.down.1
+    state.createdScopes == 3 && state.nextScope == 3
+
 #guard
   runInput? leftInput leftScope |>.any fun fixture =>
     fixture.reached.seen == ({ node := node 1, version := 1 } : SeenVersion) &&
@@ -445,51 +484,94 @@ private def closedChildren? : Option
         (BranchStart.closedTargets? factDomain children left right).isNone
     | _, _ => false
 
+#guard planError? (fun plan => plan)
+  ({ branchLimits with maxDepth := 0 }) == some .depthLimit
+
+#guard planError? (fun plan => plan)
+  ({ branchLimits with maxScopes := 2 }) == some .scopeLimit
+
 #guard
-  match runWith? splitPackages checkerInput splitPolicy limits.policy.maxDecisions with
-  | some result =>
+  planError? (fun plan =>
+    { plan with scope := { index := plan.scope.index + 1 } }) == some .wrongScope
+
+#guard
+  match splitRun?, preparedResult? with
+  | some result, some lifted =>
       match result.stop with
       | .split plan =>
-          match BranchStart.prepare
-              { branchLimits with maxDepth := 0 }
-              (BranchStart.State.start { index := 0 }) 0 result.session plan
+          match BranchStart.prepare branchLimits lifted.down.1 result.session plan
               checkerInput.target signSplitter with
-          | .error .depthLimit => true
+          | .error .wrongState => true
           | _ => false
       | _ => false
-  | none => false
+  | _, _ => false
 
 #guard
-  match splitRun? with
-  | some result =>
+  match splitRun?,
+      runWith? splitPackages checkerInput splitPolicy limits.policy.maxDecisions
+        { index := 7 } with
+  | some result, some unrelated =>
       match result.stop with
       | .split plan =>
-          let staleOrigin :=
-            { plan.origin with
-              application := { index := result.session.state.engine.applications.size } }
-          let stalePlan :=
-            { plan with
-              origin := staleOrigin
-              source := Propagator.Policy.invocationOfAction plan.scope staleOrigin }
           match BranchStart.prepare branchLimits
-              (BranchStart.State.start { index := 0 }) 0 result.session stalePlan
+              (BranchStart.State.start unrelated.session) result.session plan
               checkerInput.target signSplitter with
-          | .error .staleOrigin => true
+          | .error .wrongState => true
           | _ => false
       | _ => false
-  | none => false
+  | _, _ => false
 
 #guard
-  match runWith? splitPackages checkerInput splitPolicy limits.policy.maxDecisions with
+  planError? (fun plan =>
+    { plan with suggestion := { index := plan.suggestion.index + 1 } }) ==
+      some .unknownSuggestion
+
+-- `actionFresh` deliberately ignores the request serial; exact retained-origin
+-- authentication must still reject a serial-spliced plan.
+#guard
+  planError? (fun plan =>
+    let origin := { plan.origin with serial := plan.origin.serial + 1 }
+    { plan with
+      origin
+      source := Propagator.Policy.invocationOfAction plan.scope origin }) ==
+        some .wrongOrigin
+
+#guard
+  planError? (fun plan => { plan with point := 1 }) == some .wrongSuggestion
+
+#guard
+  planError? (fun plan => { plan with node := node 1 }) == some .wrongSuggestion
+
+#guard
+  planError? (fun plan => { plan with reason := .midpoint }) == some .wrongSuggestion
+
+#guard
+  planError? (fun plan => { plan with version := plan.version + 1 }) ==
+    some .wrongSuggestionVersion
+
+-- The branch boundary repeats the endpoint preflight instead of relying on a
+-- caller to have obtained the plan from a bounded policy view.
+#guard
+  planError? (fun plan =>
+    { plan with point := Dyadic.ofIntWithPrec 1 16 }) == some .endpointLimit
+
+#guard
+  match splitRun? with
   | some result =>
       match result.stop with
       | .split plan =>
-          match BranchStart.prepare branchLimits
-              (BranchStart.State.start { index := 0 }) 0 result.session
-              { plan with version := plan.version + 1 }
-              checkerInput.target signSplitter with
-          | .error .staleVersion => true
-          | _ => false
+          match unrelatedAction? result plan with
+          | some origin =>
+              let forged :=
+                { plan with
+                  origin
+                  source := Propagator.Policy.invocationOfAction plan.scope origin }
+              match BranchStart.prepare branchLimits
+                  (BranchStart.State.start result.session) result.session forged
+                  checkerInput.target signSplitter with
+              | .error .wrongOrigin => true
+              | _ => false
+          | none => false
       | _ => false
   | none => false
 
@@ -501,7 +583,7 @@ private def closedChildren? : Option
           let duplicate : BranchStart.Splitter Bound :=
             { split := fun _ _ _ _ _ => some (.nonnegative, .nonnegative) }
           match BranchStart.prepare branchLimits
-              (BranchStart.State.start { index := 0 }) 0 result.session plan
+              (BranchStart.State.start result.session) result.session plan
               checkerInput.target duplicate with
           | .error .duplicateChild => true
           | _ => false
diff --git a/progress/20260812T054503Z.md b/progress/20260812T054503Z.md
new file mode 100644
index 000000000..df879097e
--- /dev/null
+++ b/progress/20260812T054503Z.md
@@ -0,0 +1,37 @@
+# Branch-start authentication repair
+
+## Accomplished
+
+- Bound every branch plan to its exact retained split suggestion, including
+  the complete originating action and serial, node, point, reason, and
+  proposal-time fact version.
+- Repeated endpoint-cost validation at the branch boundary so a directly
+  constructed plan cannot bypass the engine limit.
+- Sealed branch-tree state, moved depth ownership into its active-scope table,
+  and made preparation the only operation that consumes a parent scope,
+  registers children, and advances resource counters.
+- Added discriminating conformance guards for unknown suggestions, unrelated
+  but fresh origins, changed serials, node/point/reason/version mismatches,
+  endpoint-limit bypass, wrong scopes, unrelated state, consumed state, and
+  depth/scope limits.
+- Corrected the inherited fact-lattice count and documented both the retained
+  provenance boundary and the canary tactic's remaining hard-coded Meta
+  coupling.
+- Passed focused Lean builds, repository static/trust/freshness checks, delta
+  bans, and compiled-artifact checks.
+
+## Current frontier
+
+The runtime branch inputs are authenticated against a retained engine split
+record and managed by sealed tree state. The canary Meta tactic still quotes
+fixed proof-side constants after checking equality with those inputs; it does
+not yet quote arbitrary `BranchStart.Children` dynamically.
+
+## Next step
+
+Propagate this repair through the dependent PR stack, obtain a fresh review,
+and run exact-head CI before merging the repaired edge.
+
+## Blockers
+
+None.

From 7a45abe1bb616f9dbe81676f85876bcbcaa18f19 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Fri, 14 Aug 2026 12:59:26 +0000
Subject: [PATCH 3/4] Record branch-start restack; progress 20260814T125902Z

---
 progress/20260814T125902Z.md | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 progress/20260814T125902Z.md

diff --git a/progress/20260814T125902Z.md b/progress/20260814T125902Z.md
new file mode 100644
index 000000000..53ecda57e
--- /dev/null
+++ b/progress/20260814T125902Z.md
@@ -0,0 +1,29 @@
+# Checked branch-start restack
+
+## Accomplished
+
+- Replayed #9220's branch-start feature and the retained-suggestion/state
+  repair onto merged #9219 at exact main
+  `7b25e51ea28a6783835e3bd81758941894a4b2cf`.
+- Preserved #9219's exact child reached-state, trace, side-fact, seed, and axiom
+  canaries while threading the branch manager's allocated child scopes into
+  both live sessions.
+- Retained exact plan authentication against the engine-owned suggestion,
+  endpoint limit, action, program/fact versions, and sealed scope-depth state.
+- Built the branch-start, ProofEmitter, sine, and exponential conformance
+  targets and ran structural, trust-surface, freshness, and banned-mechanism
+  checks.
+
+## Current frontier
+
+The reconciled feature is ready for force-with-lease push, direct-main
+retargeting, fresh exact-head Opus review, and exact CI.
+
+## Next step
+
+Obtain the independent review and CI result, repairing any substantive
+runtime-fidelity, accounting, provenance, or SPEC-honesty finding.
+
+## Blockers
+
+None.

From bdf897837924f52e247e5f8cf354fec3e642018b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Fri, 14 Aug 2026 13:15:31 +0000
Subject: [PATCH 4/4] Document split package ownership accurately

---
 HexInterval/Experiment/ExpSign.lean |  2 +-
 HexInterval/SPEC/hex-interval.md    | 16 ++++++++--------
 progress/20260814T131450Z.md        | 21 +++++++++++++++++++++
 3 files changed, 30 insertions(+), 9 deletions(-)
 create mode 100644 progress/20260814T131450Z.md

diff --git a/HexInterval/Experiment/ExpSign.lean b/HexInterval/Experiment/ExpSign.lean
index 595821f1f..ec3c7491d 100644
--- a/HexInterval/Experiment/ExpSign.lean
+++ b/HexInterval/Experiment/ExpSign.lean
@@ -99,7 +99,7 @@ def expRule : Registration :=
     watches := [.argument 0]
     writes := [.result] }
 
-/-- The source package may suggest zero as a domain-owned landmark.  It does
+/-- The split package may suggest zero as a domain-owned landmark.  It does
 not construct either branch. -/
 def splitRule : Registration :=
   { key := splitRuleKey
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 45e1644d7..da6e2564a 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -1599,14 +1599,14 @@ 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.
 
-The corresponding executable source package now contributes a zero-landmark
-split rule. The generic `BranchStart.prepare` transition does not trust the
-public fields of the `SplitPlan` it receives. It resolves the plan's exact
-retained suggestion identifier and requires that record to contain a split
-with the same complete action (including its request serial), node, dyadic
-cut, reason, and proposal-time fact version. It also checks the exact scope
-and reconstructs the source key from that action. The action must pass the
-retained engine's full freshness check: its application, registration,
+The corresponding executable split package now contributes a zero-landmark
+rule for the source operation. The generic `BranchStart.prepare` transition
+does not trust the public fields of the `SplitPlan` it receives. It resolves
+the plan's exact retained suggestion identifier and requires that record to
+contain a split with the same complete action (including its request serial),
+node, dyadic cut, reason, and proposal-time fact version. It also checks the
+exact scope and reconstructs the source key from that action. The action must
+pass the retained engine's full freshness check: its application, registration,
 watched versions, write authority, program-sensitive version, and structural
 matcher provenance must still match engine-owned state. The transition
 separately checks the current program version, node fact, and fact version for
diff --git a/progress/20260814T131450Z.md b/progress/20260814T131450Z.md
new file mode 100644
index 000000000..2dbee49a6
--- /dev/null
+++ b/progress/20260814T131450Z.md
@@ -0,0 +1,21 @@
+# PR #9220 exact-head review repair
+
+## Accomplished
+
+- Corrected the executable exponential split rule documentation to identify
+  the distinct split package, rather than the source package, as its owner.
+- Kept the runtime implementation and conformance surface unchanged.
+
+## Current frontier
+
+- The restacked branch-start runtime feature and retained-suggestion repair are
+  complete on current `main` with the documentation matching the package graph.
+
+## Next step
+
+- Re-run exact-head review and CI, then hand the PR back for merge if both are
+  green.
+
+## Blockers
+
+- None.