diff --git a/HexInterval/Experiment/ProofEmitter.lean b/HexInterval/Experiment/ProofEmitter.lean
index 2ca8d3879..41444fc62 100644
--- a/HexInterval/Experiment/ProofEmitter.lean
+++ b/HexInterval/Experiment/ProofEmitter.lean
@@ -414,6 +414,93 @@ def replayTransport {Fact : Type} {semantics : Semantics Fact}
       else
         none
 
+/-! ## Proof-producing solver splits -/
+
+/-- Package-owned proof boundary for one domain cut.
+
+The executable policy may propose a cut and the branch manager may compute
+candidate child facts, but neither is evidence that the children cover the
+parent.  A domain companion accepts the supplied parent, cut, and children only
+when it can prove that every value satisfying the parent lies in at least one
+child.  Binding those values to an authenticated runtime plan belongs to the
+branch layer.  Disjointness and interiority are useful search invariants, but
+are not needed for the logical join and remain branch-manager checks. -/
+structure SplitSchema (semantics : Semantics Fact) (Cut : Type) where
+  proveCover :
+    (program : Program) -> (node : NodeId) -> (parent : Fact) -> Cut ->
+      (left right : Fact) ->
+      Option
+        (Evidence
+          (forall valuation, semantics.models program valuation ->
+            semantics.holds program valuation { node, fact := parent } ->
+              semantics.holds program valuation { node, fact := left } \/
+                semantics.holds program valuation { node, fact := right }))
+
+/-- Join two conditional branch theorems using a checked coverage theorem.
+
+The child fact is an additional branch assumption, not an unconditional fact
+in the caller's context.  Facts proved before the split remain in `base` and
+are supplied identically to both children. -/
+def installSplit {Fact : Type} {semantics : Semantics Fact}
+    {program : Program} {base : List (NodeFact Fact)}
+    {node : NodeId} {parent left right : Fact} {target : NodeFact Fact}
+    (cover :
+      Evidence
+        (forall valuation, semantics.models program valuation ->
+          semantics.holds program valuation { node, fact := parent } ->
+            semantics.holds program valuation { node, fact := left } \/
+              semantics.holds program valuation { node, fact := right }))
+    (parentSound :
+      Evidence
+        (semantics.Entails program base { node, fact := parent }))
+    (leftSound :
+      Evidence
+        (semantics.Entails program ({ node, fact := left } :: base) target))
+    (rightSound :
+      Evidence
+        (semantics.Entails program ({ node, fact := right } :: base) target)) :
+    Evidence (semantics.Entails program base target) :=
+  { proof := by
+      intro valuation model baseHolds
+      have parentHolds := parentSound.proof valuation model baseHolds
+      rcases cover.proof valuation model parentHolds with leftHolds | rightHolds
+      · apply leftSound.proof valuation model
+        intro assumption member
+        rcases List.mem_cons.mp member with equal | member
+        · subst assumption
+          exact leftHolds
+        · exact baseHolds assumption member
+      · apply rightSound.proof valuation model
+        intro assumption member
+        rcases List.mem_cons.mp member with equal | member
+        · subst assumption
+          exact rightHolds
+        · exact baseHolds assumption member }
+
+/-- Transparently replay one solver split from supplied child facts.
+
+The branch searches may be arbitrary and opaque.  Their outputs enter this
+transition only as ordinary kernel evidence under the corresponding child
+assumption.  The domain schema independently proves coverage of the supplied
+children before the generic join is constructed; it does not authenticate a
+runtime plan or quotation. -/
+def replaySplit {Fact Cut : Type} {semantics : Semantics Fact}
+    (schema : SplitSchema semantics Cut) (program : Program)
+    (base : List (NodeFact Fact)) (node : NodeId) (parent : Fact) (cut : Cut)
+    (left right : Fact) (target : NodeFact Fact)
+    (parentSound :
+      Evidence
+        (semantics.Entails program base { node, fact := parent }))
+    (leftSound :
+      Evidence
+        (semantics.Entails program ({ node, fact := left } :: base) target))
+    (rightSound :
+      Evidence
+        (semantics.Entails program ({ node, fact := right } :: base) target)) :
+    Option (Evidence (semantics.Entails program base target)) := do
+  let cover <- schema.proveCover program node parent cut left right
+  pure (installSplit cover parentSound leftSound rightSound)
+
 /-- Close a requested fact from a stronger established fact at the same node.
 The independent fact-domain theorem must prove that intersecting `actual` with
 `requested` leaves `actual` unchanged.  Runtime target detection is not used
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 375cbcd6d..cb7b144cd 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -1505,6 +1505,121 @@ preserving typed session-start, run-stop, and target-probe reasons in tactic
 diagnostics remain future frontend work; none of these limitations is a
 theorem-production assumption.
 
+### Solver-split proof boundary
+
+A prepared `SplitPlan` is not a case split theorem. It proves only that an
+engine-owned offer was selected against the exact scope, program version,
+node version, current fact, and resource envelope. Three independently checked
+objects must remain distinct:
+
+1. the untrusted policy plan, which chooses where and when to split;
+2. a domain-owned coverage theorem for the exact parent fact, cut, and child
+   facts;
+3. one kernel proof of the requested target under each child assumption.
+
+The proof-side interface is polymorphic in both `Fact` and `Cut`. Its essential
+field has the following shape:
+
+```lean
+proveCover :
+  (program : Program) -> (node : NodeId) -> (parent : Fact) -> Cut ->
+    (left right : Fact) ->
+    Option (Evidence (
+      forall valuation, semantics.models program valuation ->
+        semantics.holds program valuation { node, fact := parent } ->
+          semantics.holds program valuation { node, fact := left } \/
+          semantics.holds program valuation { node, fact := right }))
+```
+
+The semantic domain package does not check executable child construction a
+second time. It independently proves only that the supplied parent, cut, and
+children have the required coverage relation; authenticating those values
+against a runtime `SplitPlan`, strict narrowing, and correct child construction
+remain separate branch-layer obligations. The current transparent
+`ProofEmitter.replaySplit` implements the generic join. Given a proof of
+`parent` from the caller's `base`, a proof of
+the target from `{node,left} :: base`, and a proof of the target from
+`{node,right} :: base`, it applies `proveCover` and returns a proof of the
+target from `base`. No policy callback, compiled session, branch score, or
+runtime comparison enters that proof. A Mathlib-free Boolean canary uses a
+nonempty inherited base; each supplied child proof explicitly consumes its
+corresponding distinct assumption as well as that base. It obtains an ordinary
+target not entailed by the empty context. Kernel-checked theorems pin both the
+demo schema's chosen child orientation and the genuine failure of two positive
+children to cover the parent. The former is a schema-format regression, not a
+logical requirement that all coverage schemas use the same orientation.
+
+Coverage is the logical requirement. Disjointness, nonempty children, and a
+strictly interior cut are search-progress requirements: omitting them cannot
+prove a false theorem, but can duplicate work or cause a split loop. The real
+interval adapter should enforce the stronger v1 convention that a dyadic cut
+produces `parent ∩ (-∞,m]` and `parent ∩ (m,+∞)`, preserving a closed boundary
+on exactly one side. Open/closed and unbounded endpoint information therefore
+lives in `Fact`; the generic join does not erase strictness or assume a closed
+interval representation. A future non-real domain may use another `Cut` type
+without changing function packages or the join theorem.
+
+Branch execution needs a provenance-aware root rather than a fresh list of
+unconditional assumptions. At a split point, facts already proved in the
+parent remain parent proofs. Exactly one new child fact is conditional on the
+corresponding case. If a child engine is restarted from the parent's complete
+fact array with the split node narrowed, its version-zero proof table must
+classify every entry as either:
+
+- an inherited parent `FactProof`, lifted into the child context; or
+- the single left or right split assumption.
+
+It must not feed all inherited derived facts to `ProofEmitter.assumed`: that
+would silently promote consequences of the caller's context into new caller
+hypotheses. The existing caller `InitialContext` is consequently not the
+branch-root API. A `BranchSeed` experiment should bind the exact child
+`initialFacts` array to this mixed proof table before chronological replay.
+
+Branches may instantiate different auxiliary expressions. Each child replay
+therefore closes its target back to the program snapshot at the split before
+the two results are joined. The package-owned `Extends` theorem and semantic
+stability law already provide the required direction: extend a split-snapshot
+model into the child program, use the child theorem there, and transport the
+old target back. Nodes, equality edges, payloads, and positive fact versions
+created below one child are scoped to that child and cannot be resolved by its
+sibling. Parent program nodes and proof terms may be shared structurally.
+
+A runtime contradiction flag is also not a closed child. The proof layer needs
+a domain-owned refutation schema which turns an exact established bottom or
+inconsistent-bound fact into `False`; generic elimination can then produce the
+branch target. Until that schema exists, a contradictory child is useful for
+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.
+
+Several operational choices deliberately remain experimental:
+
+- restart a child session from a checked snapshot, or add a sealed session-fork
+  operation which preserves reusable work and immutable payload sharing;
+- depth-first execution for small proof memory, best-first execution for early
+  target closure, or a bounded hybrid frontier;
+- store branch-local program suffixes directly, or hash-cons identical
+  instantiations above the scope layer;
+- retain `Dyadic` in real-domain executable plans while keeping the proof
+  schema generic, or replace it with a registry-resolved opaque landmark.
+
+These choices may change performance and certificate size, but not the
+coverage-and-two-proofs contract. Acceptance tests for the branch layer must
+include a useful two-sided closure, one contradiction leaf plus one target
+leaf, a nested split, a child-local instantiation, a sibling-reference attack,
+a non-interior repeated split, and fuel exhaustion with no theorem emitted.
+
+### Proof-producing frontend
+
 The fixed canary also requires a live session with no dropped work and an exact
 proof history of one instance, one equality, three fact events, and the
 expected interleaving before it reads historical values through
@@ -2040,6 +2155,105 @@ Shrinking an input does not require a rule to discard all earlier work. Cache
 reuse is a performance feature only. Every returned fact still receives a new
 or reused sound justification.
 
+## Lessons from RealPaver
+
+RealPaver is the closest concrete reference architecture for the intended
+combination of arbitrary nonlinear contractors, adaptive consistency, and
+branching. The historical claims below come from the 2004 edition 0.4 manual;
+implementation claims refer to the tagged RealPaver 1.1.1 C++ sources, rather
+than assuming that both versions expose identical algorithms. The 1.1.1
+system separates a generic `Contractor` interface, contractor composition,
+dependency-driven propagation, strong-consistency contractors, variable
+selection, and search-space order. This supports the SPEC's separation between
+package rules, engine transitions, policy, and the branch layer, but RealPaver's
+operational status values are not a proof boundary suitable for Lean.
+
+The RealPaver 1.1.1 propagation loop initially queues every contractor. After
+one contractor mutates its box, it examines only variables in that contractor's
+scope; a sufficiently large relative width reduction wakes inactive dependent
+contractors. HC4 builds one `HC4Revise` contractor per constraint over a shared
+expression DAG. BC4 associates one `ContractorBC4Revise` with each constraint;
+each such contractor first applies `ContractorHC4Revise`, then applies
+`ContractorBC3Revise` only to variables which occur more than once in that
+constraint. The source calls this combined operator hull/box consistency; it
+should not be described as pure box consistency or conflated with standalone
+BC3. The solver can compose a base HC4, BC4, or affine propagator with ACID,
+polytope relaxation, and interval Newton. This is directly translatable as:
+
+- one checked application per package contractor and an explicit watch/write
+  scope;
+- a dependency worklist rather than whole-network rescans;
+- optional stronger actions represented as additional offers, not hard-coded
+  phases in the engine;
+- policy features for relative reduction, repeated occurrences, derivative
+  influence, and recent contractor productivity.
+
+RealPaver's propagation tolerance is not a theorem. It may treat a small width
+reduction as unchanged and therefore decline to wake dependents. HexInterval
+may use the same heuristic only in policy and completion accounting: every
+accepted fact is intersected exactly, while suppressing a logically possible
+wake either belongs to an explicitly approximate profile or marks the branch
+incomplete. The tolerance can never justify `noChange`, contradiction, or
+target subsumption in emitted proof.
+
+In RealPaver 1.1.1, ACID is especially useful for the upgradeable policy
+design. It ranks variables by a derivative-based smear score, alternates
+learning and exploitation phases, measures contraction gains, and learns how
+many variable-level 3BCID contractors are worth applying. The transferable
+idea is not its particular average-gain formula. A policy-private state may
+learn an effort frontier from bounded observations and choose fewer expensive
+offers on later boxes. The engine must still own action identities, exact
+inputs, budgets, and proof payloads. Learned scores are untrusted scheduling
+data, and mutable ACID state must be branch-owned or keyed by the complete
+semantic snapshot before it is reused across siblings.
+
+RealPaver 1.1.1's variable 3BCID implementation first slices one variable, removes
+inconsistent outer slices using a nested contractor, and then applies CID to
+the remaining middle slices, returning the hull of surviving reductions. This
+maps to the `shave` action rather than a global solver split. Its Lean replay
+payload must enumerate a finite covering partition, give a checked
+contradiction for every discarded slice, give the retained contraction for
+every surviving slice, and prove the returned hull covers all survivors. A
+coarse `Empty` status from a nested run is insufficient. The number of slices,
+nested propagation work, and retained proofs are all charged to the one action.
+
+RealPaver 1.1.1 keeps solver branching separate. Its variable selectors include
+round-robin, largest/smallest domain, mixed discrete/continuous selection,
+derivative-smear selection, and hybrids. Its pending-node containers include
+DFS, BFS, distant-most DFS, and hybrids which search depth-first until a
+solution and then resume from a best pending node by depth or perimeter. These
+are useful initial policies to reproduce behind `Controller`; none belongs in
+the proof-producing core. For proof goals, additional useful scores are
+distance to a closing fact, predicted proof size, and whether both children are
+likely to close rather than average contraction alone.
+
+The principal non-transferable part of RealPaver 1.1.1 is its `Proof` enum. Its
+`Empty`, `Maybe`, `Feasible`, and `Inner` values are operational certificates
+returned by C++ methods, not kernel proof terms with replayable provenance. In
+HexInterval each successful analogue needs a package theorem or checked
+certificate tied to the exact box, constraint, and program snapshot.
+`Maybe` maps naturally to an unproved search result. `Empty` needs the
+refutation schema described in the split section. Feasible/existence results
+from interval Newton need separate existence and uniqueness theorem schemas;
+they must not be conflated with universal interval bounds.
+
+The RealPaver 0.4 manual gives small, discriminating acceptance cases:
+
+- `y = x^2` and `y = 2 - x^2` on `[0,2]^2`, where independent local
+  contraction stalls but facet shaving isolates the intersection near `(1,1)`;
+- `x*x + y^2 = 2` on `x ∈ [-2,4]`, `y ∈ [-1,1]`, where repeated occurrence
+  defeats simple hull propagation and motivates box search;
+- `x₁*x₂*x₃ = 1`, `x₁+x₂+x₃ = 0`, and
+  `max (x₁+x₂) (x₂-x₃) ≤ 0` on `[-10,10]^3`, which distinguishes one-pass
+  weak 3B, iterated 3B, and a large paving;
+- the square-system examples where interval Newton dramatically strengthens
+  local propagation, including certification of isolated roots.
+
+These should be translated into exact rational/dyadic starting boxes and
+package-owned operations. Tests compare accepted facts, branch trees, and
+proof size across policies; they do not freeze RealPaver's floating-point
+endpoints or take its output as an oracle.
+
 ## Propagation state
 
 Each live branch contains:
@@ -2617,14 +2831,15 @@ format. Its rule instead proposes a nearby dyadic guard backed by a certified
 enclosure, or handles a symbolic partition entirely inside its local proof
 payload.
 
-The concrete `Dyadic` split point and `EndpointLimit` in the current generic
-experiment are a deliberate real-domain-v1 seam, not a claim that every future
-domain or branch policy must use dyadic cuts. Keeping that seam concrete lets
-the arbitrary real-function vertical proceed without prematurely choosing
-between a cut-type parameter, a domain-owned split interface, and an opaque
-landmark decoded by the branch layer. That choice remains open and must be
-revisited before stabilizing a multi-domain API; it does not require changing
-the function-package, instantiation, or replay protocols now.
+The concrete `Dyadic` split point and `EndpointLimit` in the executable
+engine/policy protocol are a deliberate real-domain-v1 seam, not a claim that
+every future domain or runtime branch manager must use dyadic cuts. The
+proof-side `SplitSchema` is already polymorphic in its cut type. Keeping the
+runtime seam concrete lets the arbitrary real-function vertical proceed while
+the later multi-domain runtime API remains open between a domain-owned split
+interface and an opaque registry-resolved landmark. That runtime choice does
+not require changing function-package, instantiation, or proof-replay
+protocols now.
 
 A split on term `t` adds `t ≤ m` to the left child and `m < t` to the right
 child. This complementary form preserves strictness, avoids a duplicate
@@ -3361,5 +3576,20 @@ local test profile. They do not enter this Mathlib-free benchmark target.
   [An interval arithmetic for robust error estimation](https://arxiv.org/abs/2107.05784).
 - [IBEX contractor documentation](https://ibex-team.github.io/ibex-lib/contractor.html)
   and [strategy documentation](https://ibex-team.github.io/ibex-lib/strategy.html).
+- Laurent Granvilliers and Frédéric Benhamou,
+  [Algorithm 852: RealPaver, an interval solver using constraint satisfaction techniques](https://doi.org/10.1145/1132973.1132980),
+  and Laurent Granvilliers's August 2004 *RealPaver User's Manual*, edition
+  0.4, distributed in the
+  [official 0.4 source archive](https://sourceforge.net/projects/realpaver/files/realpaver/0.4/)
+  (with a [browsable manual mirror](https://manualzz.com/doc/4136960/realpaver-user-manual)).
+- Raphaël Chenouard and Laurent Granvilliers,
+  [RealPaver 1.1: A C++ Library for Constraint Programming over Numeric or Mixed Discrete-Continuous Domains](https://doi.org/10.21105/joss.09331)
+  (2026), with the
+  [tagged 1.1.1 sources](https://github.com/realpaver/realpaver/tree/v1.1.1-joss2),
+  especially the exact
+  [`IntervalPropagator`](https://github.com/realpaver/realpaver/blob/v1.1.1-joss2/src/realpaver/IntervalPropagator.cpp)
+  and
+  [`ContractorBC4Revise`](https://github.com/realpaver/realpaver/blob/v1.1.1-joss2/src/realpaver/ContractorBC4Revise.cpp)
+  implementations discussed above.
 - [IntervalArithmetic.jl construction and exact input guidance](https://juliaintervals.github.io/IntervalArithmetic.jl/stable/manual/construction/).
 - [Boost.Interval policies and representation](https://www.boost.org/doc/libs/latest/libs/numeric/interval/doc/interval.htm).
diff --git a/conformance/HexInterval/ProofEmitterConformance.lean b/conformance/HexInterval/ProofEmitterConformance.lean
index 4415d5d3b..ef944e944 100644
--- a/conformance/HexInterval/ProofEmitterConformance.lean
+++ b/conformance/HexInterval/ProofEmitterConformance.lean
@@ -194,4 +194,136 @@ theorem quotedTraceProvesContract :
   simpa [quotedStep] using
     (ProofEmitter.proofOfReplay replayed (by rfl))
 
+/-! # Generic split joining -/
+
+inductive SplitFact where
+  | all
+  | yes
+  | no
+  | enabled
+  | certified
+  deriving DecidableEq
+
+def splitNode : NodeId := node 0
+
+def splitBaseNode : NodeId := node 1
+
+def splitTargetNode : NodeId := node 2
+
+def SplitHolds (valuation : NodeId -> Bool) : NodeFact SplitFact -> Prop
+  | { fact := .all, .. } => True
+  | { node, fact := .yes } => valuation node = true
+  | { node, fact := .no } => valuation node = false
+  | { node, fact := .enabled } => valuation node = true
+  | { fact := .certified, .. } =>
+      valuation splitBaseNode = true /\
+        (valuation splitNode = true \/ valuation splitNode = false)
+
+def splitSemantics : SemanticReplay.Semantics SplitFact :=
+  { Value := Bool
+    models := fun _ _ => True
+    holds := fun _ valuation fact => SplitHolds valuation fact }
+
+def splitBase : List (NodeFact SplitFact) :=
+  [{ node := splitBaseNode, fact := .enabled }]
+
+def splitTarget : NodeFact SplitFact :=
+  { node := splitTargetNode, fact := .certified }
+
+/-- Unlike the old Boolean-decision target, certification is not true without
+the inherited base fact. -/
+theorem splitTargetNeedsBase :
+    ¬ splitSemantics.Entails program [] splitTarget := by
+  intro sound
+  let valuation : NodeId -> Bool := fun _ => false
+  have certified := sound valuation trivial (by simp)
+  exact Bool.noConfusion certified.1
+
+def splitSchema : ProofEmitter.SplitSchema splitSemantics Unit where
+  proveCover := fun _ node parent _ left right =>
+    if shape : parent = .all /\ left = .yes /\ right = .no then
+      some
+        { proof := by
+            rcases shape with ⟨rfl, rfl, rfl⟩
+            intro valuation _ _
+            cases value : valuation node with
+            | false => exact Or.inr value
+            | true => exact Or.inl value }
+    else
+      none
+
+def splitParent :
+    Evidence
+      (splitSemantics.Entails program splitBase
+        { node := splitNode, fact := .all }) :=
+  { proof := by
+      intro _ _ _
+      trivial }
+
+def splitLeft :
+    Evidence
+      (splitSemantics.Entails program
+        ({ node := splitNode, fact := .yes } :: splitBase) splitTarget) :=
+  { proof := by
+      intro valuation _ assumptions
+      have yes :=
+        assumptions { node := splitNode, fact := .yes } (by simp)
+      have enabled :=
+        assumptions { node := splitBaseNode, fact := .enabled } (by simp [splitBase])
+      exact ⟨enabled, Or.inl yes⟩ }
+
+def splitRight :
+    Evidence
+      (splitSemantics.Entails program
+        ({ node := splitNode, fact := .no } :: splitBase) splitTarget) :=
+  { proof := by
+      intro valuation _ assumptions
+      have no :=
+        assumptions { node := splitNode, fact := .no } (by simp)
+      have enabled :=
+        assumptions { node := splitBaseNode, fact := .enabled } (by simp [splitBase])
+      exact ⟨enabled, Or.inr no⟩ }
+
+def splitReplay :=
+  ProofEmitter.replaySplit splitSchema program splitBase splitNode .all () .yes .no
+    splitTarget splitParent splitLeft splitRight
+
+/-- The non-tautological target needs the inherited base fact in both branches;
+the two distinct child assumptions supply its corresponding left and right
+cases. The runtime policy and its split suggestion do not occur in the proof
+term. -/
+theorem splitCertifies :
+    splitSemantics.Entails program splitBase splitTarget :=
+  ProofEmitter.proofOfReplay splitReplay (by rfl)
+
+/-- The demo schema fixes an orientation, so this swapped quotation exercises
+that schema guard rather than a soundness requirement of the generic join. -/
+def swappedSplit :=
+  ProofEmitter.replaySplit splitSchema program splitBase splitNode .all () .no .yes
+    splitTarget splitParent splitRight splitLeft
+
+#guard swappedSplit.isNone
+
+/-- Child order is rejected by kernel reduction of the exact quoted schema
+application, independently of the executable guard above. -/
+theorem swappedSplitRejected : swappedSplit = none := by
+  rfl
+
+/-- Two copies of the positive child genuinely fail to cover the parent,
+independently of the demo schema's orientation guard. -/
+theorem yesYesNotCovering :
+    ¬ (∀ valuation, splitSemantics.models program valuation →
+      splitSemantics.holds program valuation { node := splitNode, fact := .all } →
+        splitSemantics.holds program valuation { node := splitNode, fact := .yes } ∨
+          splitSemantics.holds program valuation { node := splitNode, fact := .yes }) := by
+  intro cover
+  have covered := cover (fun _ => false) trivial trivial
+  rcases covered with yes | yes <;> exact Bool.noConfusion yes
+
+/--
+info: 'Hex.Interval.ProofEmitterConformance.splitCertifies' depends on axioms: [propext]
+-/
+#guard_msgs in
+#print axioms splitCertifies
+
 end Hex.Interval.ProofEmitterConformance
diff --git a/progress/20260811T143000Z.md b/progress/20260811T143000Z.md
new file mode 100644
index 000000000..2130cf666
--- /dev/null
+++ b/progress/20260811T143000Z.md
@@ -0,0 +1,31 @@
+# Accomplished
+
+- Added a function-agnostic, cut-type-polymorphic proof boundary for solver
+  subdivision.
+- Added the transparent join which requires a checked parent-coverage theorem
+  and ordinary target proofs under both child assumptions.
+- Added a Mathlib-free conformance theorem whose two distinct Boolean cases are
+  both consumed, plus a malformed child-order rejection.
+- Specified the provenance-aware branch root, program-extension closure,
+  contradiction-proof gap, resource accounting, and deliberately open branch
+  scheduling and storage choices.
+- Studied both the classic and current RealPaver architecture and folded its
+  dependency propagation, ACID learning/exploitation, 3BCID shaving, split
+  selectors, search-space policies, proof-boundary differences, and challenge
+  problems into the SPEC.
+
+# Current frontier
+
+The logical join exists, but a prepared runtime split is not yet executed. The
+next layer must create two scoped sessions and seed their version-zero proof
+tables from inherited parent proofs plus exactly one child assumption each.
+
+# Next step
+
+Prototype `BranchSeed`, then run one real dyadic split through two child policy
+sessions and feed both emitted target proofs to the generic join.
+
+# Blockers
+
+Contradictory leaves need a domain-owned refutation schema before they can
+close a proof branch. This does not block a first two-target-leaf vertical.
diff --git a/progress/20260811T164716Z.md b/progress/20260811T164716Z.md
new file mode 100644
index 000000000..23994569d
--- /dev/null
+++ b/progress/20260811T164716Z.md
@@ -0,0 +1,22 @@
+# Accomplished
+
+- Reconciled the proof-side split/join boundary with the repaired target
+  closure and dynamic policy-run stack.
+- Preserved the generic coverage theorem, distinct left/right child premises,
+  branch-scope design requirements, and the explicit separation between an
+  untrusted split plan and kernel case analysis.
+
+# Current frontier
+
+The proof layer can join two checked child theorems under a domain-owned cover
+theorem. It does not yet execute a retained branch tree; authenticated child
+seeding and live child sessions are the next layers in the existing stack.
+
+# Next step
+
+Finish builds and checks, push the exact head for review, then reconcile exact
+child `CheckerInput` binding and inherited-versus-split fact provenance.
+
+# Blockers
+
+None.
diff --git a/progress/20260811T170132Z.md b/progress/20260811T170132Z.md
new file mode 100644
index 000000000..5bb512c43
--- /dev/null
+++ b/progress/20260811T170132Z.md
@@ -0,0 +1,18 @@
+# Accomplished
+
+- Propagated both compile-checked modeled-goal axiom reports through the
+  split-proof boundary.
+
+# Current frontier
+
+Split coverage and joining are unchanged; the earlier generated goal proofs
+retain explicit standard-axiom regression checks.
+
+# Next step
+
+Push after the focused build, then continue through authenticated branch
+seeding and emission.
+
+# Blockers
+
+None.
diff --git a/progress/20260814T101851Z.md b/progress/20260814T101851Z.md
new file mode 100644
index 000000000..1dff289e2
--- /dev/null
+++ b/progress/20260814T101851Z.md
@@ -0,0 +1,35 @@
+# Split-proof quality repair
+
+## Accomplished
+
+- Strengthened the Mathlib-free split canary with a nonempty inherited base
+  and a target that is not entailed by the empty context. Each child proof now
+  consumes both its corresponding branch assumption and the inherited base
+  fact.
+- Added a kernel-reduced theorem that pins swapped-child rejection, alongside
+  the executable guard.
+- Corrected the SPEC's split-proof wording: semantic coverage is independent
+  evidence, not a second execution of child construction.
+- Moved the RealPaver survey out of the rule-protocol heading scope, separated
+  historical 0.4 claims from tagged 1.1.1 source claims, and described BC4's
+  precise HC4Revise-plus-BC3Revise behavior.
+- Updated the split-candidate discussion to distinguish the existing
+  cut-polymorphic proof schema from the still-dyadic executable protocol.
+- Preserved `closeFact` and the split implementation unchanged, and passed the
+  Mathlib-free focused build plus repository static, trust, freshness, line
+  count, and delta-ban checks.
+
+## Current frontier
+
+The proof combinator still intentionally accepts ordinary child evidence; the
+next stacked layers are responsible for authenticating child inputs and
+producing those proofs from live branch sessions.
+
+## Next step
+
+Propagate this quality repair through the dependent split-execution stack and
+run exact-head review and CI after the repaired commit is published.
+
+## Blockers
+
+None.
diff --git a/progress/20260814T103810Z.md b/progress/20260814T103810Z.md
new file mode 100644
index 000000000..722d8e71c
--- /dev/null
+++ b/progress/20260814T103810Z.md
@@ -0,0 +1,39 @@
+# Split-proof restack and review hardening
+
+## Accomplished
+
+- Restacked the #9216 split-proof feature and quality commits onto exact #9215
+  head `659ed4ebd434b97c79e631cffc1e4e51dd127a87`, preserving #9215's runtime
+  envelope and diagnostics paragraph at the one SPEC conflict.
+- Built the exact restacked Mathlib-free proof and target-run targets and
+  passed repository static, trust, freshness, line-count, artifact, and delta
+  ban checks.
+- Obtained a fresh isolated exact-head proof review, which found no kernel
+  soundness or trust-base blocker.
+- Reworded the proof boundary so coverage of supplied values is not confused
+  with runtime-plan quotation or authentication.
+- Distinguished the demo schema's orientation regression from logical split
+  safety, and added a kernel theorem that two positive children do not cover
+  the parent.
+- Added a pinned axiom report for the joined theorem and made every RealPaver
+  survey paragraph explicit about whether it describes the 0.4 manual or the
+  tagged 1.1.1 implementation.
+
+## Current frontier
+
+The canary's supplied child proofs explicitly use their branch assumptions and
+the inherited base, while the base is genuinely required by the target. A
+literal claim that branch assumptions are semantically necessary for the final
+entailment is not a coherent acceptance property: parent coverage together
+with both child implications is precisely a proof of that entailment from the
+base. Runtime-plan binding and branch-local program-extension bounds remain
+work for the following branch-execution layers.
+
+## Next step
+
+Push the review hardening with an exact lease, obtain a fresh review of that
+new head, and require exact-head CI to finish before merge consideration.
+
+## Blockers
+
+None.
diff --git a/progress/20260814T105429Z.md b/progress/20260814T105429Z.md
new file mode 100644
index 000000000..7f541806e
--- /dev/null
+++ b/progress/20260814T105429Z.md
@@ -0,0 +1,29 @@
+# Final split-proof review reconciliation
+
+## Accomplished
+
+- Re-anchored the repaired #9216 range without patch changes onto exact merged
+  main `eac2802519cdf3041f4208452a877abc309a6e02` and retargeted the PR to main.
+- Re-ran focused builds and repository static, trust, freshness, line-count,
+  artifact, and delta-ban checks on the main-based head.
+- Obtained a fresh isolated review of the exact main-based range; it found no
+  kernel, trust-boundary, API, resource, or inherited-behavior blocker.
+- Closed the split-proof heading before the unrelated proof-producing frontend
+  material, so the SPEC hierarchy reflects the actual section boundaries.
+- Pointed the BC4 implementation citation at the tagged `.cpp`, used exact
+  `Contractor*` class names, made the official 0.4 archive the primary manual
+  source, and cleaned up incremental paragraph reflow.
+
+## Current frontier
+
+The split-proof interface and its conformance claims are internally consistent
+and honestly defer runtime-plan authentication to the following branch layers.
+
+## Next step
+
+Push this documentation reconciliation, obtain a final fresh exact-head review,
+and require the new exact-head CI run to complete successfully before merge.
+
+## Blockers
+
+None.