interval: seed proof branches safely

HexInterval/Experiment/ProofEmitter.lean

@@ -501,6 +501,71 @@ def replaySplit {Fact Cut : Type} {semantics : Semantics Fact}
   let cover <- schema.proveCover program node parent cut left right
   pure (installSplit cover parentSound leftSound rightSound)
 
+/-! ## Provenance-safe branch roots -/
+
+/-- An established parent fact remains established after adding one child
+case assumption. -/
+def inheritSplit {Fact : Type} {semantics : Semantics Fact}
+    {program : Program} {base : List (NodeFact Fact)}
+    (side fact : NodeFact Fact)
+    (sound : Evidence (semantics.Entails program base fact)) :
+    Evidence (semantics.Entails program (side :: base) fact) :=
+  { proof := by
+      intro valuation model branchHolds
+      apply sound.proof valuation model
+      intro assumption member
+      exact branchHolds assumption (List.mem_cons_of_mem side member) }
+
+/-- The exact child case is available as the sole new branch assumption. -/
+def assumeSplit {Fact : Type} {semantics : Semantics Fact}
+    (program : Program) (base : List (NodeFact Fact)) (side : NodeFact Fact) :
+    Evidence (semantics.Entails program (side :: base) side) :=
+  assumed (by simp)
+
+/-- Proof table for every version-zero fact of a restarted child session.
+
+The exact array is runtime data, but each entry must already have an ordinary
+proof under the child context.  Inherited parent consequences therefore cannot
+be silently reclassified as caller assumptions. -/
+structure BranchSeed {Fact : Type} (semantics : Semantics Fact)
+    (input : CheckerInput Fact) (base : List (NodeFact Fact))
+    (side : NodeFact Fact) where
+  size : input.initialFacts.size = input.baseProgram.nodes.size
+  sound :
+    (node : NodeId) -> (fact : Fact) ->
+      input.initialFacts[node.index]? = some fact ->
+        Evidence
+          (semantics.Entails input.baseProgram (side :: base) { node, fact })
+
+namespace BranchSeed
+
+/-- Assemble a branch root from the one new case assumption and exact proofs
+of all nonsplit parent consequences. -/
+def make {Fact : Type} {semantics : Semantics Fact}
+    (input : CheckerInput Fact) {base : List (NodeFact Fact)}
+    (side : NodeFact Fact)
+    (size : input.initialFacts.size = input.baseProgram.nodes.size)
+    (sideAt : input.initialFacts[side.node.index]? = some side.fact)
+    (inherited :
+      (node : NodeId) -> node ≠ side.node -> (fact : Fact) ->
+        input.initialFacts[node.index]? = some fact ->
+          Evidence
+            (semantics.Entails input.baseProgram base { node, fact })) :
+    BranchSeed semantics input base side :=
+  { size
+    sound := by
+      intro node fact found
+      if same : node = side.node then
+        subst node
+        have factEq : fact = side.fact :=
+          Option.some.inj (found.symm.trans sideAt)
+        subst fact
+        exact assumeSplit input.baseProgram base side
+      else
+        exact inheritSplit side { node, fact } (inherited node same fact found) }
+
+end BranchSeed
+
 /-- 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

HexInterval/SPEC/hex-interval.md

@@ -1572,8 +1572,14 @@ classify every entry as either:
 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.
+branch-root API. The transparent `ProofEmitter.BranchSeed` now binds the exact
+child `initialFacts` array and its length to this mixed proof table. Its checked
+builder obtains the split-node entry only from the new child assumption and
+requires an inherited parent theorem for every other array entry; the
+Mathlib-free canary checks both routes, including an inherited derived fact
+which is not a literal parent base member and an unrelated top entry. The Meta
+frontend still needs to turn such a `BranchSeed` into version-zero `FactProof`
+records before chronological child replay.
 
 Branches may instantiate different auxiliary expressions. Each child replay
 therefore closes its target back to the program snapshot at the split before

conformance/HexInterval/ProofEmitterConformance.lean

@@ -326,4 +326,79 @@ info: 'Hex.Interval.ProofEmitterConformance.splitCertifies' depends on axioms: [
 #guard_msgs in
 #print axioms splitCertifies
 
+def branchBase : List (NodeFact SplitFact) :=
+  [{ node := splitBaseNode, fact := .yes }]
+
+/-- The child carries a derived parent consequence at node one, not the
+literal fact in `branchBase`. -/
+def branchInitial : Array SplitFact := #[.yes, .enabled, .all]
+
+def branchInput : CheckerInput SplitFact :=
+  { baseProgram := program
+    initialFacts := branchInitial
+    target := splitTarget }
+
+def inheritedSplitFact (observed : NodeId) (different : observed ≠ splitNode)
+    (fact : SplitFact) (found : branchInitial[observed.index]? = some fact) :
+    Evidence
+      (splitSemantics.Entails program branchBase { node := observed, fact }) :=
+  { proof := by
+      intro valuation _ assumptions
+      cases observed with
+      | mk index =>
+          cases index with
+          | zero => simp [splitNode, node] at different
+          | succ index =>
+              cases index with
+              | zero =>
+                  simp [branchInitial] at found
+                  subst fact
+                  have yes := assumptions
+                    { node := splitBaseNode, fact := .yes }
+                    (by simp [branchBase])
+                  exact yes
+              | succ index =>
+                  cases index with
+                  | zero =>
+                      simp [branchInitial] at found
+                      subst fact
+                      trivial
+                  | succ index => simp [branchInitial] at found }
+
+def branchSeed :
+    ProofEmitter.BranchSeed splitSemantics branchInput branchBase
+      { node := splitNode, fact := .yes } :=
+  ProofEmitter.BranchSeed.make branchInput { node := splitNode, fact := .yes }
+    (by rfl) (by rfl) inheritedSplitFact
+
+/-- The split node is proved from the new child assumption. -/
+example :
+    splitSemantics.Entails program
+      ({ node := splitNode, fact := .yes } :: branchBase)
+      { node := splitNode, fact := .yes } :=
+  (branchSeed.sound splitNode .yes (by rfl)).proof
+
+/-- A derived version-zero fact is inherited as a parent consequence under the
+larger child context. -/
+example :
+    splitSemantics.Entails program
+      ({ node := splitNode, fact := .yes } :: branchBase)
+      { node := splitBaseNode, fact := .enabled } :=
+  (branchSeed.sound splitBaseNode .enabled (by rfl)).proof
+
+/-- The inherited child fact above is a proved consequence, not a literal
+member of the parent base-assumption list. -/
+example :
+    ({ node := splitBaseNode, fact := .enabled } : NodeFact SplitFact) ∉
+      branchBase := by
+  simp [branchBase]
+
+/-- The unrelated version-zero top entry is also present in the exact seed
+table and has its own inherited proof. -/
+example :
+    splitSemantics.Entails program
+      ({ node := splitNode, fact := .yes } :: branchBase)
+      { node := splitTargetNode, fact := .all } :=
+  (branchSeed.sound splitTargetNode .all (by rfl)).proof
+
 end Hex.Interval.ProofEmitterConformance

progress/20260811T144508Z.md

@@ -0,0 +1,23 @@
+# Accomplished
+
+- Tightened `BranchSeed` so its program and version-zero fact array come from
+  one exact child `CheckerInput` rather than two independently supplied values.
+- Strengthened the conformance fixture with a nonempty parent context and a
+  nontrivial inherited `.yes` fact at a different node.
+- Rebuilt the Mathlib-free proof-emitter conformance target successfully.
+
+# Current frontier
+
+The child root now binds runtime input fidelity and proof provenance in the
+same type. Its split-node fact comes from the new case assumption, while an
+unchanged nontrivial fact is weakened from an established parent theorem.
+
+# Next step
+
+Have the generic Meta frontend seed its versioned evidence table from this
+exact `BranchSeed`, then replay a child trace without treating inherited parent
+consequences as caller assumptions.
+
+# Blockers
+
+None.

progress/20260811T145500Z.md

@@ -0,0 +1,24 @@
+# Accomplished
+
+- Added transparent weakening of inherited parent facts into a child context.
+- Added the exact child case as the sole new branch assumption.
+- Added `BranchSeed`, which binds every version-zero child fact and the complete
+  initial array length to ordinary evidence from one of those two routes.
+- Added conformance coverage for the split node and an unchanged inherited
+  node.
+
+# Current frontier
+
+The proof-level child root is checked. The Meta frontend does not yet translate
+it into version-zero `FactProof` records, and no child `PolicySession` is
+started yet.
+
+# Next step
+
+Add a frontend seed fold over the exact child array, then connect it to a
+restarted child session whose program snapshot is the split snapshot.
+
+# Blockers
+
+None for two target-closing children. Contradiction leaves still require the
+separate refutation schema recorded in the SPEC.

progress/20260811T150000Z.md

@@ -0,0 +1,21 @@
+# Accomplished
+
+- Bound branch version-zero proofs to the exact child `CheckerInput`.
+- Made the inherited-fact route depend on a nonempty parent context rather
+  than a trivially true top fact.
+- Completed focused conformance, repository-structure, trust, and freshness
+  checks; a fresh independent review approved the repaired design.
+
+# Current frontier
+
+The branch seed now distinguishes the one new split assumption from parent
+facts that retain their existing proofs under the larger child context.
+
+# Next step
+
+Use this seed in the generic proof frontend to initialize exact version-zero
+`FactProof` records for chronological child replay.
+
+# Blockers
+
+None.

progress/20260811T165035Z.md

@@ -0,0 +1,21 @@
+# Accomplished
+
+- Reconciled authenticated branch seeding with the repaired split/join and
+  target-closure stack.
+- Preserved exact child `CheckerInput` indexing and the distinction between
+  inherited parent proofs and the single conditional split assumption.
+
+# Current frontier
+
+Every child version-zero fact can be justified without promoting parent-derived
+facts to caller assumptions. The seed is tied to the exact child program,
+initial fact array, target, and branch side.
+
+# Next step
+
+Finish focused and static checks, push the exact head for review, then
+reconcile Meta-level emission from authenticated branch seeds.
+
+# Blockers
+
+None.

progress/20260811T170207Z.md

@@ -0,0 +1,18 @@
+# Accomplished
+
+- Propagated both compile-checked modeled-goal axiom reports through
+  authenticated branch seeding.
+
+# Current frontier
+
+Branch provenance and exact child-input binding are unchanged; inherited
+goal-proof canaries retain their explicit standard-axiom checks.
+
+# Next step
+
+Push after checks, then continue through branch proof emission and live child
+execution.
+
+# Blockers
+
+None.

progress/20260814T104145Z.md

@@ -0,0 +1,33 @@
+# Branch-seed conformance repair
+
+## Accomplished
+
+- Strengthened the Mathlib-free `BranchSeed` canary so the parent base contains
+  `{node 1, .yes}` while the child seed carries the genuinely derived,
+  non-member consequence `{node 1, .enabled}`.
+- Made the inherited proof consume the parent `.yes` theorem and establish the
+  semantically equivalent `.enabled` fact, rather than restating a literal base
+  assumption.
+- Exercised every entry of the exact three-node child seed: the split assumption
+  at node zero, the derived parent consequence at node one, and the unrelated
+  top fact at node two.
+- Kept `BranchSeed`, `BranchSeed.make`, and all public proof APIs unchanged, and
+  updated only the precise SPEC/conformance description of the stronger test.
+- Built `HexInterval.Experiment.ProofEmitter` and
+  `HexInterval.ProofEmitterConformance`; copyright, dependency-DAG, trust,
+  Phase 4, factor-freshness, diff, and added-line banned-mechanism checks pass.
+
+## Current frontier
+
+- The repair is complete as a local commit on the old PR #9217 head and is
+  ready to replay after PR #9216 merges.
+
+## Next step
+
+- Replay this commit onto the reconciled #9217 branch, rerun the focused checks,
+  and obtain exact-head review and CI there.
+
+## Blockers
+
+- None; the existing `SplitFact` semantics directly supports the stronger
+  non-member consequence.

progress/20260814T104936Z.md

@@ -0,0 +1,36 @@
+# Branch-seed stack propagation
+
+## Accomplished
+
+- Replayed the exact PR #9217 feature commit onto exact post-#9216 `main`
+  `816b3da83788c12385e71b9c66ee0f78786c7cdc`; its second parent is reviewed
+  #9216 head `ce9e9143f9d5f5d43a3d0cbba31f70dca8d74868` and its tree is identical.
+- Resolved the sole conformance insertion conflict by retaining #9216's direct
+  swapped-child rejection, noncoverage theorem, and guarded axiom report before
+  the new branch-seed canary.
+- Replayed the stronger provenance canary while adapting it to #9216's
+  `.enabled`/`.certified` split semantics: a parent `.yes` theorem establishes
+  the distinct, non-member `.enabled` child seed.
+- Pinned the split, derived, and unrelated-top entries of the exact three-node
+  initial array through `BranchSeed.sound`.
+- Preserved the `BranchSeed` structure and constructor types; only their
+  builder documentation now accurately says “nonsplit parent consequences.”
+- Built `HexInterval.Experiment.ProofEmitter` and
+  `HexInterval.ProofEmitterConformance` successfully.
+- Passed copyright, dependency-DAG, published-trust-surface, Phase 4,
+  factor-freshness, diff-whitespace, and added-line banned-mechanism checks.
+
+## Current frontier
+
+- The reconciled stack and strengthened canary are locally verified and ready
+  to push for independent exact-head review and CI.
+
+## Next step
+
+- Obtain a fresh isolated Opus verdict and exact-head GitHub Actions result;
+  leave PR #9217 unmerged.
+
+## Blockers
+
+- None. The old `.decided` test vocabulary no longer exists after #9216, but
+  `.yes` to `.enabled` expresses the same non-member provenance obligation.