From 2f14fb89bcc611a95ce4cc33481f3aba2259c940 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 17:27:10 +0000 Subject: [PATCH 1/3] feat(interval): retain bounded branch trees Progress: progress/20260811T172657Z.md --- HexInterval/Experiment/BranchTree.lean | 259 ++++++++++++++++++ HexInterval/SPEC/hex-interval.md | 45 ++- .../ExpSignConformance.lean | 111 ++++++++ lakefile.lean | 1 + progress/20260811T172657Z.md | 28 ++ progress/20260811T175219Z.md | 24 ++ .../bench/proof_only_runtime_exemptions.json | 6 + 7 files changed, 463 insertions(+), 11 deletions(-) create mode 100644 HexInterval/Experiment/BranchTree.lean create mode 100644 progress/20260811T172657Z.md create mode 100644 progress/20260811T175219Z.md diff --git a/HexInterval/Experiment/BranchTree.lean b/HexInterval/Experiment/BranchTree.lean new file mode 100644 index 000000000..e8dbf1e3e --- /dev/null +++ b/HexInterval/Experiment/BranchTree.lean @@ -0,0 +1,259 @@ +/- +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.BranchStart + +@[expose] public section + +/-! +# Resource-bounded branch trees + +This experiment retains a complete runtime tree while repeatedly running +ordinary target-directed sessions and expanding accepted split plans. It is +generic in the fact domain, executable packages, and external policy state. + +The tree is search data, not proof evidence. In particular, a runtime +contradiction leaf is not a proof of `False`, and a pair of target leaves is +not a proof of their parent target. The proof frontend must separately replay +each retained leaf and join checked child evidence through a split schema. +-/ + +namespace Hex.Interval.Experiment.BranchTree + +open Propagator PolicySession SemanticReplay TargetRun BranchStart + +/-- Which child is being initialized. Policies may use this to fork private +state differently on the two sides. -/ +inductive Side where + | left + | right + deriving DecidableEq, Repr + +/-- Replaceable pending-leaf order. -/ +inductive Order where + | depthFirst + | breadthFirst + deriving DecidableEq, Repr + +/-- Global tree resources. Child sessions retain their independent engine, +policy, and payload limits. -/ +structure Limits where + branch : BranchStart.Limits + maxSteps : Nat + maxSplits : Nat + maxLeaves : Nat + leafFuel : Nat + deriving DecidableEq, Repr + +/-- Everything needed to run and split one pending leaf. -/ +structure Config (Fact PolicyState : Type) : Type 1 where + factDomain : FactDomain Fact + packages : Array (Package Fact) + sessionLimits : PolicySession.Limits + controller : TargetRun.Controller Fact PolicyState + splitter : BranchStart.Splitter Fact + forkPolicy : PolicyState -> Side -> PolicyState + order : Order + limits : Limits + +/-- Stable index into the append-only node array. -/ +structure TreeId where + index : Nat + deriving DecidableEq, Repr + +/-- Exact input, scope, depth, and private policy state of one leaf. -/ +structure Leaf (Fact PolicyState : Type) where + scope : Propagator.Policy.ScopeId + depth : Nat + input : CheckerInput Fact + policyState : PolicyState + +/-- A leaf whose policy session can still be run. -/ +structure Job (Fact PolicyState : Type) : Type 1 where + scope : Propagator.Policy.ScopeId + depth : Nat + input : CheckerInput Fact + policyState : PolicyState + session : PolicySession.Session Fact + +/-- Why a split result was retained as a blocked leaf. -/ +inductive Blocked where + | splitRejected (error : BranchStart.Error) + | splitLimit + | leafLimit + deriving DecidableEq, Repr + +/-- Terminal runtime data for a leaf. None of these constructors is proof +evidence. -/ +inductive LeafEnd (Fact PolicyState : Type) : Type 1 + | result (run : TargetRun.Result Fact PolicyState) + | blocked (run : TargetRun.Result Fact PolicyState) (reason : Blocked) + | startError (error : PolicySession.StartError) + +/-- One retained runtime-tree node. A split node stores the exact validated +child snapshots and both child identities, even if a child session failed to +start. -/ +inductive Node (Fact PolicyState : Type) : Type 1 + | pending (job : Job Fact PolicyState) + | leaf (source : Leaf Fact PolicyState) (ending : LeafEnd Fact PolicyState) + | split (source : Leaf Fact PolicyState) + (run : TargetRun.Result Fact PolicyState) + (children : BranchStart.Children Fact) (left right : TreeId) + +/-- Monotone retained state for one tree. `leaves` counts current leaves, so +an accepted binary split increases it by exactly one. -/ +structure State (Fact PolicyState : Type) : Type 1 where + nodes : Array (Node Fact PolicyState) + frontier : List TreeId + branch : BranchStart.State + splits : Nat + leaves : Nat + steps : Nat + +/-- Failure before a coherent root tree exists. -/ +inductive StartError where + | leafLimit + | scopeLimit + | unknownTarget + | session (error : PolicySession.StartError) + deriving DecidableEq, Repr + +/-- An append-only tree should only schedule valid pending nodes. -/ +inductive Error where + | missingNode (id : TreeId) + | settledNode (id : TreeId) + deriving DecidableEq, Repr + +def sourceOf (job : Job Fact PolicyState) : Leaf Fact PolicyState := + { scope := job.scope + depth := job.depth + input := job.input + policyState := job.policyState } + +/-- A tree is settled exactly when it has no runnable leaf. It may still +contain blocked, unfinished, or failed leaves. -/ +def State.settled (state : State Fact PolicyState) : Bool := + state.frontier.isEmpty + +/-- The global processing budget may leave a nonempty frontier. -/ +def State.stepLimited (limits : Limits) (state : State Fact PolicyState) : Bool := + state.steps >= limits.maxSteps && !state.frontier.isEmpty + +/-- Build a coherent root session from the exact caller input. -/ +def start (config : Config Fact PolicyState) (scope : Propagator.Policy.ScopeId) + (input : CheckerInput Fact) (policyState : PolicyState) : + Except StartError (State Fact PolicyState) := do + if config.limits.maxLeaves = 0 then throw .leafLimit + if config.limits.branch.maxScopes = 0 then throw .scopeLimit + if (input.baseProgram.node? input.target.node).isNone then + throw StartError.unknownTarget + let session <- + match PolicySession.Session.start config.factDomain input.baseProgram + config.packages input.initialFacts config.sessionLimits scope with + | .ok session => pure session + | .error error => throw (.session error) + let root : Job Fact PolicyState := + { scope, depth := 0, input, policyState, session } + pure + { nodes := #[.pending root] + frontier := [{ index := 0 }] + branch := BranchStart.State.start scope + splits := 0 + leaves := 1 + steps := 0 } + +def schedule (order : Order) (rest fresh : List TreeId) : List TreeId := + match order with + | .depthFirst => fresh ++ rest + | .breadthFirst => rest ++ fresh + +def childNode (config : Config Fact PolicyState) (side : Side) + (scope : Propagator.Policy.ScopeId) (depth : Nat) (input : CheckerInput Fact) + (policyState : PolicyState) : Node Fact PolicyState × Bool := + let childState := config.forkPolicy policyState side + let source : Leaf Fact PolicyState := { scope, depth, input, policyState := childState } + match PolicySession.Session.start config.factDomain input.baseProgram + config.packages input.initialFacts config.sessionLimits scope with + | .ok session => + (.pending + { scope := source.scope + depth := source.depth + input := source.input + policyState := source.policyState + session }, true) + | .error error => (.leaf source (.startError error), false) + +def retainLeaf (state : State Fact PolicyState) (id : TreeId) + (source : Leaf Fact PolicyState) (ending : LeafEnd Fact PolicyState) + (rest : List TreeId) : State Fact PolicyState := + { state with + nodes := state.nodes.set! id.index (.leaf source ending) + frontier := rest + steps := state.steps + 1 } + +/-- Process one pending leaf. Split rejection and tree-resource exhaustion +are terminal leaf data; only a malformed internal frontier returns `Error`. -/ +def step [DecidableEq Fact] (config : Config Fact PolicyState) + (state : State Fact PolicyState) : Except Error (State Fact PolicyState) := do + if state.steps >= config.limits.maxSteps then return state + let some id := state.frontier.head? | return state + let rest := state.frontier.tail + let some node := state.nodes[id.index]? | throw (.missingNode id) + let .pending job := node | throw (.settledNode id) + let source := sourceOf job + let run := TargetRun.drive config.factDomain job.input.target.node + job.input.target.fact config.controller config.limits.leafFuel + job.session job.policyState + let .split plan := run.stop | + return retainLeaf state id source (.result run) rest + if state.splits >= config.limits.maxSplits then + return retainLeaf state id source (.blocked run .splitLimit) rest + if state.leaves + 1 > config.limits.maxLeaves then + return retainLeaf state id source (.blocked run .leafLimit) rest + match BranchStart.prepare config.limits.branch state.branch job.depth + run.session plan job.input.target config.splitter with + | .error error => + pure (retainLeaf state id source (.blocked run (.splitRejected error)) rest) + | .ok (branch, children) => + let leftId : TreeId := { index := state.nodes.size } + let rightId : TreeId := { index := state.nodes.size + 1 } + let (leftNode, leftPending) := childNode config .left children.leftScope + children.depth children.left run.policyState + let (rightNode, rightPending) := childNode config .right children.rightScope + children.depth children.right run.policyState + let fresh := + (if leftPending then [leftId] else []) ++ + (if rightPending then [rightId] else []) + pure + { nodes := (state.nodes.set! id.index + (.split source run children leftId rightId)).push leftNode |>.push rightNode + frontier := schedule config.order rest fresh + branch + splits := state.splits + 1 + leaves := state.leaves + 1 + steps := state.steps + 1 } + +/-- Run for at most the caller fuel and never beyond the retained global step +budget. A nonempty frontier in the result is an honest partial tree. -/ +def runFrom [DecidableEq Fact] (config : Config Fact PolicyState) : + Nat -> State Fact PolicyState -> Except Error (State Fact PolicyState) + | 0, state => pure state + | fuel + 1, state => + if state.settled || state.steps >= config.limits.maxSteps then pure state + else do + let state ← step config state + runFrom config fuel state + +termination_by fuel _ => fuel + +/-- Consume the configured global processing budget. -/ +def run [DecidableEq Fact] (config : Config Fact PolicyState) + (state : State Fact PolicyState) : Except Error (State Fact PolicyState) := + runFrom config config.limits.maxSteps state + +end Hex.Interval.Experiment.BranchTree diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 19e7cd215..5029e3aca 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1688,21 +1688,44 @@ runtime contradiction separately but deliberately refuses to treat that flag as proof closure; the frontend must first resolve an established bottom fact and apply the refutation schema described above. -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. +The first generic runtime tree manager now retains internal nodes recording +validated plans and exact child inputs, and leaves recording target, +contradiction, saturation, resource failure, split refusal, session-start +failure, or any other precise `TargetRun` result. It stores the append-only +node array and a separate pending frontier, so a global step limit returns an +honest partial tree rather than relabelling unexplored leaves as closed. +Independent limits bound processed leaves, accepted splits, current leaf +count, split depth, total created scopes, and each leaf run's policy fuel in +addition to the per-session engine and payload limits. Split- and leaf-limit +exhaustion is retained at the exact parent leaf. A child session which cannot +start is likewise retained beside its sibling instead of silently deleting +the branch. + +The manager is function- and representation-independent. Its configuration +supplies the fact domain, runtime packages, controller, splitter, child-policy +fork, and pending order. The initial orders are depth-first and breadth-first; +their frontier transformation is separately tested so later best-first or +hybrid queues do not affect branch validation. The exponential conformance +tree selects the authenticated root split, starts both exact scoped children, +runs the arbitrary exponential propagator in each, and retains two target +leaves. Separate guards show that one global step leaves both children pending, +and that zero split or one-leaf budgets retain an explicitly blocked root. + +This runtime tree contains no proof evidence. The existing two-child proof +canary separately demonstrates how exact retained child runs can be replayed +and joined, but the manager does not yet emit that term. The proof-tree layer +must emit a theorem only when every coverage child is closed by replay or a +checked refutation. For best-bound mode, unfinished leaves must contribute +their inherited parent fact to the global hull; they never inherit a tighter +sibling fact. 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; +- use the delivered depth-first or breadth-first list frontier, or replace it + with best-first execution or a bounded hybrid without changing retained + nodes; - 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 @@ -1731,7 +1754,7 @@ we decide which parts belong in the Mathlib-free runtime and Mathlib semantic companion. Remaining acceptance tests include a theorem whose proof mathematically requires branching, a nested split, a child-local instantiation, a sibling-reference attack, a non-interior repeated split, and -fuel exhaustion with no theorem emitted. +proof emission refusing the delivered step-limited partial tree. ### Proof-producing frontend diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean index 628f38e0e..f94f12760 100644 --- a/conformance/HexIntervalMathlib/ExpSignConformance.lean +++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean @@ -10,6 +10,7 @@ import HexInterval.Experiment.GoalClosure import HexInterval.Experiment.ProofFrontend import HexInterval.Experiment.TargetRun import HexInterval.Experiment.BranchStart +import HexInterval.Experiment.BranchTree import Mathlib.Lean.Elab.Tactic.Meta /-! @@ -590,6 +591,116 @@ private def closedChildren? : Option | _ => false | none => false +/-! ## Retained resource-bounded branch trees -/ + +/-- Split only at the root; in each exact child, select the exponential +propagator. This deliberately keeps scheduling policy outside the generic +tree manager. -/ +private def treePolicy : TargetRun.Controller Bound Unit := + { update := fun state _ => state + choose := fun state view => + let selected := + if view.scope.index == 0 then splitOffer? view + else view.offers.toList.find? (invokesExpAt (node 1)) + match selected with + | some offer => .select offer state + | none => .stop state } + +private def treeLimits (maxSteps := 3) (maxSplits := 1) + (maxLeaves := 2) : BranchTree.Limits := + { branch := branchLimits + maxSteps + maxSplits + maxLeaves + leafFuel := limits.policy.maxDecisions } + +private def treeConfig (resources : BranchTree.Limits) : + BranchTree.Config Bound Unit := + { factDomain + packages := splitPackages + sessionLimits := limits + controller := treePolicy + splitter := signSplitter + forkPolicy := fun state _ => state + order := .depthFirst + limits := resources } + +private def runTree? (resources : BranchTree.Limits) : + Option (BranchTree.State Bound Unit) := do + let .ok state := BranchTree.start (treeConfig resources) { index := 0 } + checkerInput () | none + let .ok state := BranchTree.run (treeConfig resources) state | none + some state + +private def targetLeaf (expectedScope : Nat) (expectedSource : Bound) + (treeNode : BranchTree.Node Bound Unit) : Bool := + match treeNode with + | .leaf source (.result result) => + source.scope.index == expectedScope && source.depth == 1 && + source.input.initialFacts == #[expectedSource, .all] && + match result.stop with + | .target reached => + reached.seen == ({ node := node 1, version := 1 } : SeenVersion) && + reached.fact == .nonnegative && + result.session.state.engine.facts == #[expectedSource, .nonnegative] + | _ => false + | _ => false + +#guard + runTree? (treeLimits) |>.any fun state => + state.nodes.size == 3 && state.frontier.isEmpty && state.settled && + state.steps == 3 && state.splits == 1 && state.leaves == 2 && + match state.nodes[0]?, state.nodes[1]?, state.nodes[2]? with + | some (BranchTree.Node.split source _ children left right), + some leftNode, some rightNode => + source.scope.index == 0 && source.depth == 0 && + source.input.baseProgram == checkerInput.baseProgram && + source.input.initialFacts == checkerInput.initialFacts && + source.input.target == checkerInput.target && + children.leftScope.index == 1 && + children.rightScope.index == 2 && left.index == 1 && right.index == 2 && + targetLeaf 1 .nonnegative leftNode && targetLeaf 2 .negative rightNode + | _, _, _ => false + +/- One global step retains the exact split and both runnable children; it does +not claim that either child or the tree is complete. -/ +#guard + runTree? (treeLimits (maxSteps := 1)) |>.any fun state => + state.nodes.size == 3 && state.steps == 1 && state.splits == 1 && + state.leaves == 2 && state.frontier == [{ index := 1 }, { index := 2 }] && + state.stepLimited (treeLimits (maxSteps := 1)) && + match state.nodes[1]?, state.nodes[2]? with + | some (BranchTree.Node.pending _), some (BranchTree.Node.pending _) => true + | _, _ => false + +#guard + runTree? (treeLimits (maxSplits := 0)) |>.any fun state => + state.nodes.size == 1 && state.frontier.isEmpty && state.splits == 0 && + state.leaves == 1 && + match state.nodes[0]? with + | some (BranchTree.Node.leaf _ + (BranchTree.LeafEnd.blocked _ BranchTree.Blocked.splitLimit)) => true + | _ => false + +#guard + runTree? (treeLimits (maxLeaves := 1)) |>.any fun state => + state.nodes.size == 1 && state.frontier.isEmpty && state.splits == 0 && + state.leaves == 1 && + match state.nodes[0]? with + | some (BranchTree.Node.leaf _ + (BranchTree.LeafEnd.blocked _ BranchTree.Blocked.leafLimit)) => true + | _ => false + +#guard + BranchTree.schedule .depthFirst [{ index := 9 }] + [{ index := 1 }, { index := 2 }] == + [{ index := 1 }, { index := 2 }, { index := 9 }] + +#guard + BranchTree.schedule .breadthFirst [{ index := 9 }] + [{ index := 1 }, { index := 2 }] == + [{ index := 9 }, { index := 1 }, { index := 2 }] + /-! ## Operation-composed semantics at an arbitrary graph node -/ private def nestedInstruction : Node := diff --git a/lakefile.lean b/lakefile.lean index 52adcea5e..8ca8ae677 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -308,6 +308,7 @@ lean_lib HexIntervalExperiment where `HexInterval.Experiment.PolicySession, `HexInterval.Experiment.TargetRun, `HexInterval.Experiment.BranchStart, + `HexInterval.Experiment.BranchTree, `HexInterval.Experiment.SemanticReplay, `HexInterval.Experiment.ChronologicalReplay, `HexInterval.Experiment.GenericInstanceReconstruction, diff --git a/progress/20260811T172657Z.md b/progress/20260811T172657Z.md new file mode 100644 index 000000000..c274458aa --- /dev/null +++ b/progress/20260811T172657Z.md @@ -0,0 +1,28 @@ +# Accomplished + +- Added a function-independent retained branch-tree manager with exact root + and child inputs, append-only nodes, replaceable DFS/BFS frontiers, and + global step, split, leaf, depth, scope, and per-leaf fuel bounds. +- Retained split rejection, tree-resource exhaustion, child-start failure, and + unfinished runs explicitly instead of treating them as closure. +- Ran a live exponential tree from an authenticated root split through two + separately scoped child sessions and checked the completed and partial-tree + shapes. +- Updated the SPEC to distinguish this runtime tree from later proof-tree + emission. + +# Current frontier + +The runtime manager can retain and schedule a complete two-child tree, but it +does not yet turn that tree into a proof term. The existing fixed two-child +frontend remains the proof-producing reference path. + +# Next step + +Connect the retained useful ReLU tree to a generic bottom-up proof-tree emitter, +then add a genuinely nested split so DFS/BFS policy choices are exercised on +live pending work. + +# Blockers + +None. diff --git a/progress/20260811T175219Z.md b/progress/20260811T175219Z.md new file mode 100644 index 000000000..192cd86a8 --- /dev/null +++ b/progress/20260811T175219Z.md @@ -0,0 +1,24 @@ +# Accomplished + +- Rebased the retained branch-tree experiment onto the corrected ReLU SPEC + base while preserving the exact-blob factor-freshness exemption. +- Preserved the distinction between branch-dependent child rules and the + unconditional final ReLU theorem during conflict resolution. +- Corrected the remaining acceptance-test wording to name the delivered + step-limited partial tree rather than an untested per-leaf fuel stop. +- Passed the factor-freshness and exact-diff checks on the rebased tree. + +# Current frontier + +The retained tree is honest runtime search data with exact resource accounting, +but generic proof-tree emission and a nested scheduling canary remain later +layers. + +# Next step + +Obtain a fresh exact-head review and exact-head CI result, then let the generic +proof-tree layer consume this final base. + +# Blockers + +None. diff --git a/scripts/bench/proof_only_runtime_exemptions.json b/scripts/bench/proof_only_runtime_exemptions.json index 087a406e2..984be9b2f 100644 --- a/scripts/bench/proof_only_runtime_exemptions.json +++ b/scripts/bench/proof_only_runtime_exemptions.json @@ -161,6 +161,12 @@ "current_blob": "52adcea5e56f2c241816ea1cf3613b859c60ae40", "reason": "Additionally registers the fixed-data endpoint-valued sin-ten chronology experiment, its proof-only real-semantics companion, and conformance modules; the factorization service target and executable dependency graph are unchanged." }, + { + "path": "lakefile.lean", + "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56", + "current_blob": "8ca8ae6777b592a0ebc5ae18ffa6db130a4de7e4", + "reason": "Additionally registers the isolated Mathlib-free HexInterval branch-tree experiment only; the factorization service target and executable dependency graph are unchanged." + }, { "path": "HexBerlekamp/FactorTacticTests.lean", "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59", From ff58bc9a2c3dbb08c22cdef88a7c61e622264696 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 18:03:03 +0000 Subject: [PATCH 2/3] fix(interval): reconcile retained branch state --- HexInterval/Experiment/BranchTree.lean | 6 +++--- progress/20260811T172657Z.md | 6 +++--- progress/20260814T180230Z.md | 30 ++++++++++++++++++++++++++ 3 files changed, 36 insertions(+), 6 deletions(-) create mode 100644 progress/20260814T180230Z.md diff --git a/HexInterval/Experiment/BranchTree.lean b/HexInterval/Experiment/BranchTree.lean index e8dbf1e3e..4226dc863 100644 --- a/HexInterval/Experiment/BranchTree.lean +++ b/HexInterval/Experiment/BranchTree.lean @@ -162,7 +162,7 @@ def start (config : Config Fact PolicyState) (scope : Propagator.Policy.ScopeId) pure { nodes := #[.pending root] frontier := [{ index := 0 }] - branch := BranchStart.State.start scope + branch := BranchStart.State.start session splits := 0 leaves := 1 steps := 0 } @@ -215,8 +215,8 @@ def step [DecidableEq Fact] (config : Config Fact PolicyState) return retainLeaf state id source (.blocked run .splitLimit) rest if state.leaves + 1 > config.limits.maxLeaves then return retainLeaf state id source (.blocked run .leafLimit) rest - match BranchStart.prepare config.limits.branch state.branch job.depth - run.session plan job.input.target config.splitter with + match BranchStart.prepare config.limits.branch state.branch run.session plan + job.input.target config.splitter with | .error error => pure (retainLeaf state id source (.blocked run (.splitRejected error)) rest) | .ok (branch, children) => diff --git a/progress/20260811T172657Z.md b/progress/20260811T172657Z.md index c274458aa..068982f9b 100644 --- a/progress/20260811T172657Z.md +++ b/progress/20260811T172657Z.md @@ -19,9 +19,9 @@ frontend remains the proof-producing reference path. # Next step -Connect the retained useful ReLU tree to a generic bottom-up proof-tree emitter, -then add a genuinely nested split so DFS/BFS policy choices are exercised on -live pending work. +Connect a retained distinct-assumption ReLU tree to a generic bottom-up +proof-tree emitter, then add a genuinely nested split so DFS/BFS policy choices +are exercised on live pending work. # Blockers diff --git a/progress/20260814T180230Z.md b/progress/20260814T180230Z.md new file mode 100644 index 000000000..3e49856c9 --- /dev/null +++ b/progress/20260814T180230Z.md @@ -0,0 +1,30 @@ +# PR #9224 reconciliation + +## Accomplished + +- Replayed only the retained runtime branch-tree feature onto exact current + `main` `055eaeb92a1b25105261b65d018dbf37da50aaa6`, preserving the merged + refutation, ReLU, PNT-log, Machin, and endpoint-sine work. +- Updated the tree to seed sealed branch state from the exact root session and + to use the current depth-owning `BranchStart.prepare` API. +- Preserved exact append-only nodes, child inputs, scopes, policy snapshots, + partial frontiers, and monotone step, split, and leaf accounting. +- Refreshed the narrow lakefile factor-freshness exemption to the exact + branch-tree registration blob; the factorization executable graph is + unchanged. +- Kept proof emission explicitly outside the runtime tree and retained every + unfinished, blocked, or child-start-failure leaf without claiming closure. + +## Current frontier + +- The function-independent runtime tree executes the live two-child + exponential canary. Nested live scheduling and generic proof-tree emission + remain later layers. + +## Next step + +- Complete focused/static checks, fresh exact-head review, and exact-head CI. + +## Blockers + +- None. From 1acf751ce8f3ee92d78ca90c795bbb6618340e59 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 18:12:32 +0000 Subject: [PATCH 3/3] docs(interval): retain both partial-tree tests --- HexInterval/SPEC/hex-interval.md | 9 +++++---- progress/20260814T180230Z.md | 2 ++ 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 5029e3aca..320885777 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1749,12 +1749,13 @@ replays them, and `replaySplit` produces the joined entailment evidence. `closeRelu` specializes that evidence to the ordinary theorem `0 ≤ max x 0`. Each rule rejects the unsplit top fact, and mutating either quote to use its sibling's assumption makes emission fail. The package remains a compact -conformance fixture while -we decide which parts belong in the Mathlib-free runtime and Mathlib semantic +conformance fixture while we decide which parts belong in the Mathlib-free +runtime and Mathlib semantic companion. Remaining acceptance tests include a theorem whose proof mathematically requires branching, a nested split, a child-local -instantiation, a sibling-reference attack, a non-interior repeated split, and -proof emission refusing the delivered step-limited partial tree. +instantiation, a sibling-reference attack, a non-interior repeated split, +per-leaf fuel exhaustion with no theorem emitted, and proof emission refusing +the delivered step-limited partial tree. ### Proof-producing frontend diff --git a/progress/20260814T180230Z.md b/progress/20260814T180230Z.md index 3e49856c9..176bffbd5 100644 --- a/progress/20260814T180230Z.md +++ b/progress/20260814T180230Z.md @@ -14,6 +14,8 @@ unchanged. - Kept proof emission explicitly outside the runtime tree and retained every unfinished, blocked, or child-start-failure leaf without claiming closure. +- Kept per-leaf fuel exhaustion and proof refusal for a global step-limited + partial tree as separate future acceptance tests. ## Current frontier