diff --git a/HexInterval/Experiment/ProofFrontend.lean b/HexInterval/Experiment/ProofFrontend.lean
index 66fd458cf..53f9eaa0d 100644
--- a/HexInterval/Experiment/ProofFrontend.lean
+++ b/HexInterval/Experiment/ProofFrontend.lean
@@ -160,6 +160,44 @@ def closeTarget [BEq Fact] (context : Context Fact Handle)
         actualTerm, requestedTerm, established.proof]
   replayResult result
 
+/-- Emit a package-owned refutation of one exact established fact version.
+
+The recognizer table only selects a declaration.  The emitted
+`ProofEmitter.replayRefute` application rechecks that declaration against the
+exact fact and can produce the target only when the fact's proof is already in
+the chronology evidence table. -/
+def refuteFact [BEq Fact] (context : Context Fact Handle)
+    (state : State Fact) (table : RefuteTable Fact Handle)
+    (seen : SeenVersion) (fact : Fact) (target : NodeFact Fact) : MetaM Expr := do
+  let some established := findFact? state.known seen fact
+    | throwError "interval frontend: refuted fact version has not been proved"
+  let some handle := table.find? fact
+    | throwError "interval frontend: no unique refutation schema accepts the fact"
+  let declaration ← context.resolveSchema handle
+  discard <| getConstInfo declaration
+  let exactFact ← context.encoder.nodeFact { node := seen.node, fact }
+  let targetTerm ← context.encoder.nodeFact target
+  let result ←
+    mkAppM ``ProofEmitter.replayRefute
+      #[mkConst declaration, state.program, context.baseFactsTerm,
+        exactFact, targetTerm, established.proof]
+  replayResult result
+
+/-- Select a refutable fact from supplied fact/version snapshot arrays, require
+that exact node, version, and fact in the proof table, and emit arbitrary target
+closure from its semantic impossibility.
+
+The arrays are untrusted selector data; the live caller supplies its retained
+engine arrays. Runtime contradiction state is intentionally not an argument,
+and only the chronology proof found in `state` enters the emitted theorem. -/
+def refuteCurrent [BEq Fact] (context : Context Fact Handle)
+    (state : State Fact) (table : RefuteTable Fact Handle)
+    (facts : Array Fact) (versions : Array Nat) (target : NodeFact Fact) :
+    MetaM Expr := do
+  let some (seen, fact, _) := table.current? facts versions
+    | throwError "interval frontend: no current fact has a unique refutation schema"
+  refuteFact context state table seen fact target
+
 /-- Seed caller-owned version-zero facts by exact positions in the base list. -/
 def seedBase (context : Context Fact Handle) (program : Expr) (basePrefix : Expr) :
     MetaM (List (FactProof Fact)) := do
diff --git a/HexInterval/Experiment/ProofRegistry.lean b/HexInterval/Experiment/ProofRegistry.lean
index 48b054531..85cfcafe4 100644
--- a/HexInterval/Experiment/ProofRegistry.lean
+++ b/HexInterval/Experiment/ProofRegistry.lean
@@ -13,39 +13,83 @@ public import HexInterval.Experiment.ProofEmitter
 /-!
 # Joint semantic and proof-emitter package assembly
 
-An executable propagator package, its semantic replay schemas, and its tactic
-emission handles are three views of one extension point.  This module keeps
-the latter two views in one descriptor and checks them against the executable
-registry in the same package order.
+An executable propagator package, its semantic replay schemas, its tactic
+emission handles, and any fact-domain refutation declarations are views of one
+extension point.  This module keeps the proof-facing views in one descriptor
+and checks event schemas against the executable registry in the same package
+order.
 
-The full replay key includes the rule, event role, and payload schema.  Joint
+The full event replay key includes the rule, event role, and payload schema.  Joint
 assembly requires exact package-local equality of those keys: an emitter may
 neither omit a semantic schema nor borrow one from another package.  The
 frontend therefore remains function-agnostic without maintaining a second,
-potentially divergent registry by hand.
+potentially divergent registry by hand. Refutations have no engine event key;
+their exact-fact recognizers are only untrusted selectors for kernel-checked
+`RefuteSchema` applications.
 -/
 
 namespace Hex.Interval.Experiment.ProofRegistry
 
 open Propagator PayloadArena SemanticReplay ProofEmitter
 
+/-- One package-owned recognizer and declaration handle for contradictory
+facts.  Recognition is untrusted planning: the selected declaration must still
+return a `RefuteSchema` accepting the exact fact when the emitted application
+is kernel checked. -/
+structure RefuteRef (Fact Handle : Type) where
+  accepts : Fact → Bool
+  handle : Handle
+
+/-- Refutation recognizers assembled in package order.  More than one match is
+ambiguous and therefore has no selected handle. -/
+structure RefuteTable (Fact Handle : Type) where
+  entries : List (RefuteRef Fact Handle)
+
+namespace RefuteTable
+
+/-- Select the unique package-owned refutation declaration for one exact fact. -/
+def find? (table : RefuteTable Fact Handle) (fact : Fact) : Option Handle :=
+  match table.entries.filter (fun entry => entry.accepts fact) with
+  | [entry] => some entry.handle
+  | _ => none
+
+/-- Select the first current fact with one unambiguous refutation declaration.
+The returned version and fact are the exact values later required from the
+proof table; array mismatch or absence fails closed. -/
+def current? (table : RefuteTable Fact Handle) (facts : Array Fact)
+    (versions : Array Nat) : Option (SeenVersion × Fact × Handle) := do
+  if facts.size != versions.size then none
+  for index in [0:facts.size] do
+    let some fact := facts[index]? | none
+    let some version := versions[index]? | none
+    if let some handle := table.find? fact then
+      return ({ node := { index }, version }, fact, handle)
+  none
+
+end RefuteTable
+
 /-- The proof-facing declarations contributed by one executable package.
 
-`semantic` contains the package-owned checkers and the corresponding `emit`
-fragment contains exactly the handles a tactic may use to apply them. -/
+`semantic` contains the package-owned event checkers, the corresponding `emit`
+fragment contains exactly the handles a tactic may use to apply them, and
+`refute` contributes optional contradiction-leaf declarations. -/
 structure Package (semantics : Semantics Fact) (Handle : Type) where
   semantic : SemanticReplay.Package semantics
   emit : EmitPackage Handle
+  refute : List (RefuteRef Fact Handle) := []
 
 /-- A semantic registry and emitter table assembled from the same packages. -/
 structure Registry (semantics : Semantics Fact) (Handle : Type) where
   private mk ::
   semantic : SemanticReplay.Registry semantics
   emit : SchemaTable Handle
+  refute : RefuteTable Fact Handle
 
-private def make (semantic : SemanticReplay.Registry semantics)
-    (emit : SchemaTable Handle) : Registry semantics Handle :=
-  { semantic, emit }
+private def make {Fact Handle : Type} {semantics : Semantics Fact}
+    (semantic : SemanticReplay.Registry semantics)
+    (emit : SchemaTable Handle) (refute : RefuteTable Fact Handle) :
+    Registry semantics Handle :=
+  { semantic, emit, refute }
 
 /-- Failures specific to joint proof-package assembly.
 
@@ -128,6 +172,9 @@ opaque build (executable : Propagator.Registry Fact)
   | .ok _ =>
       match SchemaTable.build emitPackages with
       | none => throw BuildError.invalidEmit
-      | some emit => pure (make semantic emit)
+      | some emit =>
+          let refute :=
+            { entries := packages.toList.flatMap (fun package => package.refute) }
+          pure (make semantic emit refute)
 
 end Hex.Interval.Experiment.ProofRegistry
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index e90968157..632b18dbb 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -1654,10 +1654,22 @@ contains the bottom fact; the conformance obligations are successful
 transparent replay, rejection of the satisfiable `.all` fact, and the guarded
 kernel-dependency report. No engine flag or evaluator result enters that
 theorem.
-Connecting a retained contradictory fact and its emitted evidence to this
-schema inside the tree frontend remains open. An unexplored, fuel-limited,
-resource-limited, incomplete, or merely saturated child likewise does not
-close the parent target.
+
+`ProofRegistry.Package` also contributes optional fact recognizers and
+refutation handles. Lookup accepts exactly one matching handle; no match or an
+ambiguous match fails closed. The low-level frontend treats its supplied fact
+and version arrays as untrusted selector data; the live child passes its exact
+retained engine arrays. For any selected fact, the frontend requires the same
+node, version, and value in its chronology evidence table before it applies the
+schema and produces the child target by ordinary elimination. Arbitrary arrays
+cannot create evidence, but this helper does not itself certify their identity
+with an engine snapshot. Its first mixed join splits the exponential output:
+the left child closes directly from `.nonnegative`, while the right child
+starts from `.negative`, replays the exponential proposal to derive `.empty`,
+and closes only through `replayRefute`. The runtime contradiction result
+selects this path but is not an argument to any emitted proof combinator. An
+unexplored, fuel-limited, resource-limited, incomplete, or merely saturated
+child likewise does not close the parent target.
 
 The later proof-plan sketch represents an endpoint contradiction by two
 `FactId`s, whereas `replayRefute` deliberately consumes one exact established
@@ -1665,8 +1677,8 @@ fact. Its frontend lowering must therefore either resolve an already-installed
 contradictory meet fact or combine the two retained proofs through the domain's
 `FactDomainSchema.proveMeet` theorem before invoking the refutation schema.
 That lowering must first check that both identifiers name facts at the same
-node. The two-proof bridge remains open; it is not a capability of the current
-single-fact conformance canary.
+node. The current frontend consumes an already-installed single contradictory
+fact; the two-proof lowering remains part of the open tree-frontend bridge.
 
 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
@@ -1700,10 +1712,12 @@ These choices may change performance and certificate size, but not the
 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.
+assumption. The mixed target/refutation join does consume the two incompatible
+output assumptions, but useful non-contradictory branch-dependent reasoning
+remains a separate acceptance test. Remaining acceptance tests include that
+useful two-sided closure, 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
 
@@ -1755,16 +1769,26 @@ safety comes from constant lookup, ordinary Lean typechecking, and the replay
 transition's exact key check; only the resulting well-typed theorem
 application enters the kernel.
 `ProofRegistry.Package` now joins each package's semantic schemas and emitter
-fragment. Joint assembly first uses the semantic registry check to establish
-exact package-for-package ownership and bidirectional coverage against the
+fragment, plus any domain-level refutation recognizers owned by that package.
+Joint assembly first uses the semantic registry check to establish exact
+package-for-package ownership and bidirectional coverage against the
 executable formats. It then requires package-local equality of semantic and
-emitter replay-key sets and global emitter uniqueness. Consequently a handle
-cannot be omitted, added under an undeclared key, or borrowed from another
-package even if the final flattened key set would happen to match. The live
-real-sine semantic replay and direct-emission table are both projections of
-this one checked registry. This governance relation is still defense in depth
-rather than part of theorem soundness: every selected schema must produce the
-required kernel-checked claim.
+emitter replay-key sets and global emitter uniqueness. Consequently an event
+handle cannot be omitted, added under an undeclared key, or borrowed from
+another package even if the final flattened key set would happen to match.
+Refutation handles have no executable event key; exact-fact lookup instead
+requires a unique matching recognizer, and the selected `RefuteSchema` must
+accept the same fact during kernel-checked replay. The live real-sine semantic
+replay and direct-emission table are both projections of this one checked
+registry. This governance relation is still defense in depth rather than part
+of theorem soundness: every selected schema must produce the required
+kernel-checked claim.
+
+The current real adapter places its domain-wide `.empty` refuter in the source
+proof package solely to give it one registry-owned lookup position. The theorem
+is about fact-domain bottom semantics, not the source operation. A second
+matching owner would make lookup ambiguous and fail closed; a future explicit
+domain-schema home may replace this provisional ownership convention.
 
 A Mathlib companion must instantiate those abstract schemas, decode each
 frozen entry independently of package cache state, and recheck the
diff --git a/HexIntervalMathlib/Experiment/ExpSign.lean b/HexIntervalMathlib/Experiment/ExpSign.lean
index a20d19786..3cc25521a 100644
--- a/HexIntervalMathlib/Experiment/ExpSign.lean
+++ b/HexIntervalMathlib/Experiment/ExpSign.lean
@@ -173,9 +173,16 @@ def expEmit : EmitPackage Lean.Name :=
       [{ key := expFactSchema.key
          handle := ``expFactSchema }] }
 
+/-- The source package is the designated registry owner for the domain-wide
+bottom refuter. This ownership supplies one unambiguous lookup position; the
+`.empty` theorem itself is fact-domain semantics, not source-operation
+semantics. -/
 def sourceProof : ProofRegistry.Package semantics Lean.Name :=
   { semantic := { factSchemas := #[] }
-    emit := sourceEmit }
+    emit := sourceEmit
+    refute :=
+      [{ accepts := fun fact => fact == .empty
+         handle := ``emptyRefute }] }
 
 def expProof : ProofRegistry.Package semantics Lean.Name :=
   { semantic := { factSchemas := #[expFactSchema] }
diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean
index b601491ae..26325cc56 100644
--- a/conformance/HexIntervalMathlib/ExpSignConformance.lean
+++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean
@@ -1155,4 +1155,301 @@ example : True := by
       throwError "interval_exp test: stale rule version was accepted"
   trivial
 
+/-! ## One proved child joined with one proof-refuted child -/
+
+private def outputSplitKey : RuleKey :=
+  { name := "exp-sign.output.split-zero" }
+
+private def outputSplitRule : Registration :=
+  { key := outputSplitKey
+    head := expKey
+    kind := .split
+    watches := [.result]
+    writes := [] }
+
+private def outputSplitPackage : Package Bound :=
+  { Cache := Unit
+    cache := ()
+    requiredOperations := #[expOperation]
+    handlers :=
+      #[Handler.statelessDroppingDrafts outputSplitRule splitInvoke] }
+
+private def outputSplitPackages : Array (Package Bound) :=
+  #[sourcePackage, expPackage, outputSplitPackage]
+
+private def outputSplitOffer? (view : Propagator.Policy.View Bound) :
+    Option Propagator.Policy.OfferView :=
+  view.offers.toList.find? fun offer =>
+    match offer.key with
+    | .invoke invocation => invocation.rule == outputSplitKey
+    | .split _ target _ _ => target.node == node 1
+    | _ => false
+
+private def outputSplitPolicy : TargetRun.Controller Bound Unit :=
+  { update := fun state _ => state
+    choose := fun state view =>
+      match outputSplitOffer? view with
+      | some offer => .select offer state
+      | none => .stop state }
+
+private def outputPrepared? : Option (ULift.{1, 0} (BranchStart.Children Bound)) :=
+  match runWith? outputSplitPackages checkerInput outputSplitPolicy
+      limits.policy.maxDecisions with
+  | some result =>
+      match result.stop with
+      | .split plan =>
+          match BranchStart.prepare branchLimits
+              (BranchStart.State.start result.session) result.session plan
+              checkerInput.target signSplitter with
+          | .ok (_, children) => some (ULift.up children)
+          | .error _ => none
+      | _ => none
+  | none => none
+
+private def outputFact (side : Bound) : NodeFact Bound :=
+  { node := node 1, fact := side }
+
+private def outputFacts (side : Bound) : List (NodeFact Bound) :=
+  outputFact side :: baseFacts
+
+private def outputInitial (side : Bound) : Array Bound := #[.all, side]
+
+private def outputInput (side : Bound) : CheckerInput Bound :=
+  { baseProgram := program
+    initialFacts := outputInitial side
+    target := checkerInput.target }
+
+private def outputLeftInput : CheckerInput Bound := outputInput .nonnegative
+private def outputRightInput : CheckerInput Bound := outputInput .negative
+private def outputLeftFacts : List (NodeFact Bound) := outputFacts .nonnegative
+private def outputRightFacts : List (NodeFact Bound) := outputFacts .negative
+private def outputLeftScope : Propagator.Policy.ScopeId := { index := 1 }
+private def outputRightScope : Propagator.Policy.ScopeId := { index := 2 }
+
+private def inheritOutput (side : Bound) (observed : NodeId)
+    (different : observed ≠ node 1) (fact : Bound)
+    (found : (outputInput 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 [outputInput, outputInitial] at found
+              subst fact
+              exact assumptions _ (by simp [baseFacts, node])
+          | succ index =>
+              cases index with
+              | zero => simp [node] at different
+              | succ index => simp [outputInput, outputInitial] at found }
+
+private def outputLeftSeed :
+    ProofEmitter.BranchSeed semantics outputLeftInput baseFacts
+      (outputFact .nonnegative) :=
+  ProofEmitter.BranchSeed.make outputLeftInput (outputFact .nonnegative)
+    (by rfl) (by rfl) (inheritOutput .nonnegative)
+
+private def outputRightSeed :
+    ProofEmitter.BranchSeed semantics outputRightInput baseFacts
+      (outputFact .negative) :=
+  ProofEmitter.BranchSeed.make outputRightInput (outputFact .negative)
+    (by rfl) (by rfl) (inheritOutput .negative)
+
+private theorem outputWithin (side : Bound) :
+    FactsWithin program (outputFacts side) := by
+  intro fact member
+  simp only [outputFacts, outputFact, baseFacts, List.mem_cons,
+    List.not_mem_nil, or_false] at member
+  rcases member with rfl | rfl | rfl <;> simp [program, node]
+
+private def outputLeftContext : ProofFrontend.Context Bound Name :=
+  splitContext (mkConst ``outputLeftInput) (mkConst ``outputLeftFacts)
+    (mkApp (mkConst ``outputWithin) (mkConst ``Bound.nonnegative))
+    outputLeftFacts
+
+private def outputRightContext : ProofFrontend.Context Bound Name :=
+  splitContext (mkConst ``outputRightInput) (mkConst ``outputRightFacts)
+    (mkApp (mkConst ``outputWithin) (mkConst ``Bound.negative))
+    outputRightFacts
+
+private def outputParent : Evidence
+    (semantics.Entails program baseFacts (outputFact .all)) :=
+  ProofEmitter.assumed (by simp [baseFacts, outputFact, node])
+
+private def sameChecker (left right : CheckerInput Bound) : Bool :=
+  left.baseProgram == right.baseProgram &&
+    left.initialFacts == right.initialFacts && left.target == right.target
+
+#guard
+  outputPrepared?.any fun lifted =>
+    let children := lifted.down
+    children.depth == 1 && sameChecker children.parent checkerInput &&
+      sameChecker children.left outputLeftInput &&
+      sameChecker children.right outputRightInput &&
+      children.leftScope == outputLeftScope &&
+      children.rightScope == outputRightScope
+
+#guard
+  runRaw? outputLeftInput firstOffer limits.policy.maxDecisions
+      outputLeftScope |>.any fun result =>
+    match result.stop with
+    | .target reached =>
+        reached.seen == ({ node := node 1, version := 0 } : SeenVersion) &&
+          reached.fact == .nonnegative && result.events.isEmpty
+    | _ => false
+
+#guard
+  runRaw? outputRightInput firstOffer limits.policy.maxDecisions
+      outputRightScope |>.any fun result =>
+    match result.stop with
+    | .contradiction =>
+        result.session.state.engine.facts == #[.all, .empty] &&
+          result.session.state.engine.versions == #[0, 1] &&
+          result.events.size == 1
+    | _ => false
+
+#guard
+  fixture?.any fun fixture =>
+    fixture.registry.refute.find? .empty == some ``emptyRefute &&
+      fixture.registry.refute.find? .all == none
+
+private meta def emitOutputTarget (input : CheckerInput Bound)
+    (scope : Propagator.Policy.ScopeId) : MetaM Expr := do
+  let some result := runRaw? input firstOffer limits.policy.maxDecisions scope
+    | throwError "interval_exp_refute: target child did not start"
+  let .target reached := result.stop
+    | throwError "interval_exp_refute: target child did not close"
+  let .ok registry := ProofRegistry.build result.session.registry proofPackages
+    | throwError "interval_exp_refute: target child registry failed"
+  let some trace := Frontend.trace? result.session.state.engine result.session.arena
+    | throwError "interval_exp_refute: target child quotation failed"
+  let state ← ProofFrontend.emitBranch outputLeftContext input
+    (mkConst ``outputLeftSeed) trace.program trace.events registry.emit
+  ProofFrontend.closeTarget outputLeftContext state reached.seen reached.fact
+    input.target
+
+private meta def emitOutputRefute (input : CheckerInput Bound)
+    (scope : Propagator.Policy.ScopeId) : MetaM Expr := do
+  let some result := runRaw? input firstOffer limits.policy.maxDecisions scope
+    | throwError "interval_exp_refute: contradiction child did not start"
+  let .contradiction := result.stop
+    | throwError "interval_exp_refute: contradiction child did not contradict"
+  let .ok registry := ProofRegistry.build result.session.registry proofPackages
+    | throwError "interval_exp_refute: contradiction child registry failed"
+  let some trace := Frontend.trace? result.session.state.engine result.session.arena
+    | throwError "interval_exp_refute: contradiction child quotation failed"
+  unless trace.program == input.baseProgram do
+    throwError "interval_exp_refute: contradiction trace changed the graph"
+  let [.rule step] := trace.events
+    | throwError "interval_exp_refute: contradiction trace is not exactly one rule"
+  unless 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 == .empty && step.event.version == 1 &&
+      step.previous == .negative do
+    throwError "interval_exp_refute: contradiction rule trace drifted"
+  let state ← ProofFrontend.emitBranch outputRightContext input
+    (mkConst ``outputRightSeed) trace.program trace.events registry.emit
+  ProofFrontend.refuteCurrent outputRightContext state registry.refute
+    result.session.state.engine.facts result.session.state.engine.versions
+    input.target
+
+private meta def emitOutputSplitRefute : MetaM Expr := do
+  let some lifted := outputPrepared?
+    | throwError "interval_exp_refute: output split was not prepared"
+  let children := lifted.down
+  unless sameChecker children.left outputLeftInput &&
+      sameChecker children.right outputRightInput do
+    throwError "interval_exp_refute: prepared children differ from proof contexts"
+  let left ← emitOutputTarget children.left children.leftScope
+  let right ← emitOutputRefute children.right children.rightScope
+  let result ←
+    mkAppM ``ProofEmitter.replaySplit
+      #[mkConst ``signSplit, mkConst ``program, mkConst ``baseFacts,
+        ← boundEncoder.nodeId (node 1), ← boundEncoder.fact .all,
+        mkConst ``Unit.unit, ← boundEncoder.fact .nonnegative,
+        ← boundEncoder.fact .negative,
+        ← boundEncoder.nodeFact checkerInput.target,
+        mkConst ``outputParent, left, right]
+  ProofFrontend.replayResult result
+
+private meta def proveSplitRefute (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 ← emitOutputSplitRefute
+            let proof ← mkAppM ``closeExp #[mkFVar declaration.fvarId, evidence]
+            unless ← isDefEq (← inferType proof) target do
+              throwError "interval_exp_refute: joined proof has the wrong target"
+            return (← instantiateMVars proof)
+          saved.restore
+      | none => saved.restore
+  throwError "interval_exp_refute: expected a goal `0 ≤ Real.exp x`"
+
+syntax (name := intervalExpRefuteTac) "interval_exp_refute" : tactic
+
+@[tactic intervalExpRefuteTac] meta def evalIntervalExpRefute : Tactic := fun stx => do
+  match stx with
+  | `(tactic| interval_exp_refute) =>
+      let goal ← getMainGoal
+      goal.withContext do
+        goal.assign (← proveSplitRefute (← instantiateMVars (← goal.getType)))
+      replaceMainGoal []
+  | _ => throwUnsupportedSyntax
+
+/-- The left branch closes from its split assumption; the right branch uses
+its incompatible assumption to derive `.empty`, proves that exact fact
+impossible, and only then participates in the parent join. -/
+theorem tacticExpRefutedBranch (x : ℝ) : 0 ≤ Real.exp x := by
+  interval_exp_refute
+
+/--
+info: 'Hex.IntervalMathlib.ExpSignConformance.tacticExpRefutedBranch' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound]
+-/
+#guard_msgs in
+#print axioms tacticExpRefutedBranch
+
+/-- Failure on an unsupported target restores the tactic state. -/
+example (x : ℝ) : x = x := by
+  fail_if_success interval_exp_refute
+  rfl
+
+set_option linter.unusedTactic false in
+example : True := by
+  run_tac
+    let some result := runRaw? outputRightInput firstOffer
+        limits.policy.maxDecisions outputRightScope
+      | throwError "interval_exp_refute test: missing contradictory child"
+    let .ok registry := ProofRegistry.build result.session.registry proofPackages
+      | throwError "interval_exp_refute test: child registry failed"
+    let some trace := Frontend.trace? result.session.state.engine result.session.arena
+      | throwError "interval_exp_refute test: child quotation failed"
+    let state ← ProofFrontend.emitBranch outputRightContext outputRightInput
+      (mkConst ``outputRightSeed) trace.program trace.events registry.emit
+    let moved := result.session.state.engine.facts.set! 0 .empty
+    if (← observing? <| ProofFrontend.refuteCurrent outputRightContext state
+        registry.refute moved result.session.state.engine.versions
+        outputRightInput.target).isSome then
+      throwError "interval_exp_refute test: bottom at an unproved node was accepted"
+    let changed := result.session.state.engine.facts.set! 1 .all
+    if (← observing? <| ProofFrontend.refuteCurrent outputRightContext state
+        registry.refute changed result.session.state.engine.versions
+        outputRightInput.target).isSome then
+      throwError "interval_exp_refute test: changed bottom fact was accepted"
+    let stale := result.session.state.engine.versions.set! 1 0
+    if (← observing? <| ProofFrontend.refuteCurrent outputRightContext state
+        registry.refute result.session.state.engine.facts stale
+        outputRightInput.target).isSome then
+      throwError "interval_exp_refute test: stale bottom version was accepted"
+  trivial
+
 end Hex.IntervalMathlib.ExpSignConformance
diff --git a/conformance/HexIntervalMathlib/ProofRegistryConformance.lean b/conformance/HexIntervalMathlib/ProofRegistryConformance.lean
index fe759ff91..b226fb526 100644
--- a/conformance/HexIntervalMathlib/ProofRegistryConformance.lean
+++ b/conformance/HexIntervalMathlib/ProofRegistryConformance.lean
@@ -121,4 +121,22 @@ private def wrongRolePackages :
     | .error (.missingEmit 2 key) => key == sineFactSchema.key
     | _ => false
 
+private def oneRefute : RefuteTable Nat Nat :=
+  { entries := [{ accepts := fun fact => fact == 7, handle := 11 }] }
+
+private def ambiguousRefute : RefuteTable Nat Nat :=
+  { entries :=
+      [{ accepts := fun fact => fact == 7, handle := 11 },
+       { accepts := fun fact => fact == 7, handle := 12 }] }
+
+#guard oneRefute.find? 7 == some 11 && oneRefute.find? 8 == none
+
+#guard ambiguousRefute.find? 7 == none
+
+#guard
+  oneRefute.current? #[3, 7] #[4, 9] ==
+    some ({ node := { index := 1 }, version := 9 }, 7, 11)
+
+#guard (oneRefute.current? #[7] #[3, 4]).isNone
+
 end Hex.IntervalMathlib.ProofRegistryConformance
diff --git a/progress/20260811T154649Z.md b/progress/20260811T154649Z.md
new file mode 100644
index 000000000..0908e7227
--- /dev/null
+++ b/progress/20260811T154649Z.md
@@ -0,0 +1,29 @@
+# Accomplished
+
+- Added package-owned refutation recognizers and handles to the generic proof
+  registry, with unique exact-fact lookup and deterministic current-fact
+  selection.
+- Added generic frontend emission from an exact retained fact/version and its
+  chronology proof to a package-owned `RefuteSchema`.
+- Added a live mixed branch canary: the left exponential-output child closes
+  from its `.nonnegative` split assumption, while the right child uses its
+  `.negative` assumption and the exponential rule to establish `.empty`, then
+  closes only by semantic refutation.
+- Added an ordinary kernel theorem for the mixed join, exact runtime guards,
+  ambiguous-refuter rejection, and a stale-bottom-version mutation test.
+
+# Current frontier
+
+One target child and one proof-refuted child can now participate in the same
+generic split join without placing runtime contradiction state in the proof.
+The registry's refutation recognizers are planning data; the emitted schema
+application remains the trust boundary.
+
+# Next step
+
+Reconcile the branch-start freshness repair, then move from this two-leaf
+canary to a retained tree node with nested split and live-leaf accounting.
+
+# Blockers
+
+None.
diff --git a/progress/20260811T163039Z.md b/progress/20260811T163039Z.md
new file mode 100644
index 000000000..0745835b6
--- /dev/null
+++ b/progress/20260811T163039Z.md
@@ -0,0 +1,26 @@
+# Accomplished
+
+- Rebased the mixed target/refutation branch frontend onto exact refutation
+  commit `ad82f6ae6ad609d83b2e581d6a9d0aa3832830da` without incorporating the
+  separate ReLU prototype.
+- Verified that package-owned refutation lookup, exact current fact/version
+  selection, and the live one-target/one-refuted-child join compose with the
+  authenticated branch runtime and split-enabled proof registry.
+- Built the exponential and proof-registry conformance targets and reran
+  trust-surface, phase, DAG, source-lint, and proof-only freshness checks.
+
+# Current frontier
+
+An exact retained bottom fact can now be selected through a package-owned
+refutation table, tied back to chronology evidence at the same version, and
+used as one side of a kernel-checked split join. Runtime contradiction state
+remains outside the proof term.
+
+# Next step
+
+Add retained tree nodes, nested split execution, and live-leaf accounting while
+keeping target and proof-refuted leaf closure as separate checked cases.
+
+# Blockers
+
+None.
diff --git a/progress/20260811T165719Z.md b/progress/20260811T165719Z.md
new file mode 100644
index 000000000..97d1c8d55
--- /dev/null
+++ b/progress/20260811T165719Z.md
@@ -0,0 +1,22 @@
+# Accomplished
+
+- Reconciled the refutation frontend and mixed target/refuted-child join with
+  the repaired branch runtime and refutation proof layer.
+- Preserved exact refutation-schema selection, exact fact/version proof lookup,
+  and the non-vacuous join in which one child closes the target normally while
+  the other produces `False` from an established bottom fact.
+
+# Current frontier
+
+The frontend can close a mixed two-child split without trusting runtime stop
+state. Selector overlap currently fails closed; explicit registry governance
+for overlapping refutation recognizers remains future hardening.
+
+# Next step
+
+Finish focused and static checks, push the exact head for review, and ensure
+the useful branch-dependent ReLU vertical is restacked on this repaired base.
+
+# Blockers
+
+None.
diff --git a/progress/20260811T170502Z.md b/progress/20260811T170502Z.md
new file mode 100644
index 000000000..d49e874d6
--- /dev/null
+++ b/progress/20260811T170502Z.md
@@ -0,0 +1,18 @@
+# Accomplished
+
+- Propagated both compile-checked modeled-goal axiom reports through the mixed
+  target/refuted-child frontend.
+
+# Current frontier
+
+Mixed branch closure is unchanged; inherited generated goal proofs retain
+explicit standard-axiom checks.
+
+# Next step
+
+Push after focused builds and notify the useful ReLU branch to restack on this
+exact base.
+
+# Blockers
+
+None.
diff --git a/progress/20260814T153454Z.md b/progress/20260814T153454Z.md
new file mode 100644
index 000000000..36d04fada
--- /dev/null
+++ b/progress/20260814T153454Z.md
@@ -0,0 +1,33 @@
+# PR #9222 reconciliation
+
+## Accomplished
+
+- Replayed only the refutation-registry/frontend and mixed-child feature onto
+  exact current `main`, retaining the merged #9221 proof and honesty repairs.
+- Updated the live split preparation call to the sealed branch state API that
+  derives its root scope from the exact engine-owned session.
+- Reconciled the contradiction SPEC so the delivered single-fact frontend and
+  the still-open two-`FactId` same-node lowering are stated separately.
+- Clarified that fact/version arrays are untrusted selector data: the live
+  path supplies the retained engine arrays, while evidence requires the exact
+  node, version, and fact from the chronology proof table.
+- Added a guarded dependency report for the mixed theorem, an unsupported-goal
+  state-restoration canary, and rejection of a mutated bottom-fact snapshot.
+- Pinned the prepared parent/depth and the exact right-child `.negative` to
+  `.empty` trace, and exercised exact chronology rejection for a fake bottom at
+  the wrong node.
+
+## Current frontier
+
+- One live child closes the target normally and the other derives `.empty`,
+  resolves its unique package refuter, and closes through ordinary proof
+  replay without putting runtime contradiction state in evidence.
+
+## Next step
+
+- Run the complete focused/static gates, push and retarget the PR, then obtain
+  a fresh exact-head independent review and exact-head CI.
+
+## Blockers
+
+- None.