From 4c5ed04e66b178e2a59bb6908a920856c8e2c9cb Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 17:25:48 +0000 Subject: [PATCH 1/8] Propagate provenance honesty through ReLU branch; progress 20260811T171522Z --- HexInterval/SPEC/hex-interval.md | 14 +- .../ExpSignConformance.lean | 548 ++++++++++++++++++ progress/20260811T153755Z.md | 32 + progress/20260811T155115Z.md | 25 + progress/20260811T165120Z.md | 28 + 5 files changed, 644 insertions(+), 3 deletions(-) create mode 100644 progress/20260811T153755Z.md create mode 100644 progress/20260811T155115Z.md create mode 100644 progress/20260811T165120Z.md diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 62a6ae254..a7cacd6b6 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1713,9 +1713,17 @@ 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. 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 +output assumptions. A separate conformance-local max-zero/ReLU package now +supplies the first useful non-contradictory branch-dependent vertical. Its +nonnegative rule proves `max x 0 = x` only from the left split fact; its strict +negative rule proves `max x 0 = 0` only from the right split fact. Both child +sessions retain one ordinary rule event with the exact side fact as an input, +the unchanged generic frontend replays them, and `replaySplit` produces 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 companion. Remaining +acceptance tests include a nested split, a child-local instantiation, a sibling-reference attack, a non-interior repeated split, and fuel exhaustion with no theorem emitted. diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean index 26325cc56..20dcaed1b 100644 --- a/conformance/HexIntervalMathlib/ExpSignConformance.lean +++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean @@ -1452,4 +1452,552 @@ example : True := by throwError "interval_exp_refute test: stale bottom version was accepted" trivial +/-! ## Branch-dependent ReLU propagation + +Unlike exponential positivity, these two propagators are intentionally +conditional. The nonnegative-side rule proves `max x 0 = x` from `0 <= x`; +the negative-side rule proves `max x 0 = 0` from `x < 0`. The runtime and +proof packages know those two function-specific facts, while branch creation, +branch seeding, chronology replay, and the two-proof join stay generic. -/ + +private def reluKey : OpKey := { name := "relu-sign.max-zero" } + +private def reluNonnegativeKey : RuleKey := + { name := "relu-sign.max-zero.nonnegative" } + +private def reluNegativeKey : RuleKey := + { name := "relu-sign.max-zero.negative" } + +private def reluOperation : Operation := + { key := reluKey, inputs := [real], output := real } + +private def reluOperations : Array Operation := #[sourceOperation, reluOperation] + +private def reluInstruction : Node := + { domain := real, op := { index := 1 }, args := [node 0] } + +private def reluProgram : Program := + { operations := reluOperations, nodes := #[sourceInstruction, reluInstruction] } + +private def reluNonnegativeRule : Registration := + { key := reluNonnegativeKey + head := reluKey + kind := .forward + watches := [.argument 0] + writes := [.result] } + +private def reluNegativeRule : Registration := + { key := reluNegativeKey + head := reluKey + kind := .forward + watches := [.argument 0] + writes := [.result] } + +private def reluFormat (side : Bound) : ReplayFormat := + { role := .fact + schema := 1 + validateBody := fun body => body == [side.code] } + +private def reluPlan (side : Bound) (request : RuleRequest Bound) : Plan Bound := + match request.inputs, request.writes with + | [source], [target] => + if source.fact == side then + { outcome := + .success + [{ node := target, fact := .nonnegative, payload := payload 0 }] + [] {} + drafts := + [{ label := payload 0 + role := .fact + schema := 1 + body := [side.code] }] } + else + { outcome := .failed 10, drafts := [] } + | _, _ => { outcome := .failed 11, drafts := [] } + +private def reluPackage : Package Bound := + { Cache := Unit + cache := () + operations := #[reluOperation] + handlers := + #[Handler.statelessPlanned reluNonnegativeRule + (reluPlan .nonnegative) #[reluFormat .nonnegative], + Handler.statelessPlanned reluNegativeRule + (reluPlan .negative) #[reluFormat .negative]] } + +private def reluPackages : Array (Package Bound) := #[sourcePackage, reluPackage] + +private def reluSplitPackages : Array (Package Bound) := + #[sourcePackage, reluPackage, splitPackage] + +private def reluModel : OperationSemantics.Model ℝ := + { operation := reluOperation + relation := fun inputs output => + match inputs with + | [input] => output = max input 0 + | _ => False } + +private def reluModels : Array (OperationSemantics.Model ℝ) := + #[sourceModel, reluModel] + +private def reluSemantics : Semantics Bound := + OperationSemantics.semantics reluModels Contains + +private def reluBoundSchema : FactDomainSchema reluSemantics := + { top := fun _ => .all + topSound := by + intro _ _ _ _ _ _ + trivial + proveMeet := fun _ _ previous proposed installed => + if exact : installed = previous.meet proposed then + some + { proof := by + subst installed + intro valuation _ + exact containsMeet previous proposed (valuation _) } + else + none } + +private def reluLaws : Laws reluSemantics := + { holdsEq := by + intro _ valuation left right fact _ _ values + change Contains fact (valuation left) ↔ Contains fact (valuation right) + rw [values] } + +private def reluStableLaw : GenericInstanceReconstruction.StableLaw reluSemantics := + OperationSemantics.stableLaw reluModels Contains + +private def reluSplitSchema : SplitSchema reluSemantics Unit where + proveCover := fun _ _ parent _ left right => + if shape : parent = .all ∧ left = .nonnegative ∧ right = .negative then + some + { proof := by + rcases shape with ⟨rfl, rfl, rfl⟩ + intro valuation _ _ + change NodeId → ℝ at valuation + change (0 : ℝ) ≤ valuation _ ∨ valuation _ < 0 + exact le_or_gt 0 (valuation _) } + else + none + +private theorem reluSideEntails (side : Bound) + (accepted : side = .nonnegative ∨ side = .negative) + (graph : Program) (assumptions : List (NodeFact Bound)) + (output : NodeId) (instruction : Node) (input : NodeId) + (found : graph.node? output = some instruction) + (operation : instruction.op = { index := 1 }) + (arguments : instruction.args = [input]) + (exactAssumptions : assumptions = [{ node := input, fact := side }]) : + reluSemantics.Entails graph assumptions + { node := output, fact := .nonnegative } := by + change ∀ valuation : NodeId → ℝ, + OperationSemantics.Models reluModels graph valuation → + (∀ assumption, assumption ∈ assumptions → + Contains assumption.fact (valuation assumption.node)) → + Contains .nonnegative (valuation output) + intro valuation model holds + obtain ⟨meaning, meaningAt, related⟩ := + model.2 output instruction found + simp [reluModels, operation] at meaningAt + subst meaning + have outputEq : valuation output = max (valuation input) 0 := by + simpa [reluModel, arguments, List.map] using related + have inputH : Contains side (valuation input) := + holds { node := input, fact := side } (by simp [exactAssumptions]) + rcases accepted with rfl | rfl + · change (0 : ℝ) ≤ valuation output + rw [outputEq, max_eq_left inputH] + exact inputH + · change (0 : ℝ) ≤ valuation output + change valuation input < 0 at inputH + rw [outputEq, max_eq_right inputH.le] + +private theorem reluFactWith (fact : NodeFact Bound) {value : Bound} + (equal : fact.fact = value) : + fact = { node := fact.node, fact := value } := by + cases fact + simp_all + +private def reluFactSchema (key : RuleKey) (side : Bound) + (accepted : side = .nonnegative ∨ side = .negative) : + PackedFactSchema reluSemantics where + rule := key + schema := 1 + Certificate := Unit + decode := fun body => if body == [side.code] then some () else none + replay := fun _ _ context _ => + if proposedFact : context.proposed.fact = .nonnegative then + match found : context.program.node? context.proposed.node with + | some instruction => + if operation : instruction.op = ({ index := 1 } : OpId) then + match arguments : instruction.args with + | [input] => + if exactAssumptions : + context.assumptions = [{ node := input, fact := side }] then + some + { proof := by + have proposedEq : + context.proposed = + { node := context.proposed.node, + fact := .nonnegative } := + reluFactWith context.proposed proposedFact + rw [proposedEq] + exact + reluSideEntails side accepted context.program + context.assumptions context.proposed.node instruction + input found operation arguments exactAssumptions } + else + none + | _ => none + else + none + | none => none + else + none + +private def reluNonnegativeSchema : PackedFactSchema reluSemantics := + reluFactSchema reluNonnegativeKey .nonnegative (Or.inl rfl) + +private def reluNegativeSchema : PackedFactSchema reluSemantics := + reluFactSchema reluNegativeKey .negative (Or.inr rfl) + +private def reluSourceProof : ProofRegistry.Package reluSemantics Name := + { semantic := { factSchemas := #[] } + emit := { schemas := [] } } + +private def reluProof : ProofRegistry.Package reluSemantics Name := + { semantic := + { factSchemas := #[reluNonnegativeSchema, reluNegativeSchema] } + emit := + { schemas := + [{ key := reluNonnegativeSchema.key, + handle := ``reluNonnegativeSchema }, + { key := reluNegativeSchema.key, + handle := ``reluNegativeSchema }] } } + +private def reluProofPackages : + Array (ProofRegistry.Package reluSemantics Name) := + #[reluSourceProof, reluProof] + +private def reluBaseFacts : List (NodeFact Bound) := + [{ node := node 0, fact := .all }, { node := node 1, fact := .all }] + +private def reluInput : CheckerInput Bound := + { baseProgram := reluProgram + initialFacts := #[.all, .all] + target := { node := node 1, fact := .nonnegative } } + +private theorem reluBaseWithin : FactsWithin reluProgram reluBaseFacts := by + intro fact member + simp only [reluBaseFacts, List.mem_cons, List.not_mem_nil, or_false] at member + rcases member with rfl | rfl <;> simp [reluProgram, node] + +private theorem reluBasePrefix : ProgramPrefix reluProgram reluProgram := + ProgramPrefix.refl reluProgram + +private theorem reluSameOperations : + reluProgram.operations = reluProgram.operations := rfl + +private def reluInitialExtension : + Evidence (reluSemantics.Extends reluProgram reluProgram) := + extendRefl reluSemantics reluProgram + +private noncomputable def reluValuation (x : ℝ) : NodeId → ℝ + | ⟨0⟩ => x + | ⟨1⟩ => max x 0 + | _ => 0 + +private theorem reluValuationModels (x : ℝ) : + reluSemantics.models reluProgram (reluValuation x) := by + refine ⟨?_, ?_⟩ + · simp [reluProgram, reluOperations, reluModels, sourceModel, reluModel] + rintro ⟨index⟩ instruction found + cases index with + | zero => + simp [Program.node?, reluProgram, sourceInstruction] at found + subst instruction + exact ⟨sourceModel, by rfl, by rfl⟩ + | succ index => + cases index with + | zero => + simp [Program.node?, reluProgram, reluInstruction] at found + subst instruction + exact ⟨reluModel, by rfl, by rfl⟩ + | succ index => + simp [Program.node?, reluProgram] at found + +private theorem closeRelu (x : ℝ) + (result : Evidence + (reluSemantics.Entails reluProgram reluBaseFacts reluInput.target)) : + 0 ≤ max x 0 := by + have holds := result.proof (reluValuation x) (reluValuationModels x) + (by + intro fact member + simp only [reluBaseFacts, List.mem_cons, List.not_mem_nil, or_false] at member + rcases member with rfl | rfl <;> trivial) + exact holds + +private def reluOffer? (key : RuleKey) (view : Propagator.Policy.View Bound) : + Option Propagator.Policy.OfferView := + view.offers.toList.find? fun offer => + match offer.key with + | .invoke invocation => invocation.rule == key + | _ => false + +private def reluRulePolicy (key : RuleKey) : + TargetRun.Controller Bound Unit := + { update := fun state _ => state + choose := fun state view => + match reluOffer? key view with + | some offer => .select offer state + | none => .stop state } + +private def reluRunWith? (runtimePackages : Array (Package Bound)) + (input : CheckerInput Bound) (controller : TargetRun.Controller Bound Unit) + (scope : Propagator.Policy.ScopeId := { index := 0 }) : + Option (TargetRun.Result Bound Unit) := do + let .ok session := PolicySession.Session.start factDomain + input.baseProgram runtimePackages input.initialFacts limits scope + | none + some (TargetRun.drive factDomain input.target.node input.target.fact controller + limits.policy.maxDecisions session ()) + +private def reluPrepared? : + Option (ULift.{1, 0} (BranchStart.Children Bound)) := + match reluRunWith? reluSplitPackages reluInput splitPolicy with + | none => none + | some result => + match result.stop with + | .split plan => + match BranchStart.prepare branchLimits + (BranchStart.State.start { index := 0 }) 0 result.session plan + reluInput.target signSplitter with + | .ok (_, children) => some (ULift.up children) + | .error _ => none + | _ => none + +private def reluBranchFact (side : Bound) : NodeFact Bound := + { node := node 0, fact := side } + +private def reluBranchFacts (side : Bound) : List (NodeFact Bound) := + reluBranchFact side :: reluBaseFacts + +private def reluBranchInput (side : Bound) : CheckerInput Bound := + { baseProgram := reluProgram + initialFacts := #[side, .all] + target := reluInput.target } + +private def reluInherit (side : Bound) (observed : NodeId) + (different : observed ≠ node 0) (fact : Bound) + (found : (reluBranchInput side).initialFacts[observed.index]? = some fact) : + Evidence + (reluSemantics.Entails reluProgram reluBaseFacts { node := observed, fact }) := + { proof := by + intro _ _ assumptions + cases observed with + | mk index => + cases index with + | zero => simp [node] at different + | succ index => + cases index with + | zero => + simp [reluBranchInput] at found + subst fact + exact assumptions _ (by simp [reluBaseFacts, node]) + | succ index => simp [reluBranchInput] at found } + +private def reluLeftInput : CheckerInput Bound := + reluBranchInput .nonnegative + +private def reluRightInput : CheckerInput Bound := + reluBranchInput .negative + +private def reluLeftFacts : List (NodeFact Bound) := + reluBranchFacts .nonnegative + +private def reluRightFacts : List (NodeFact Bound) := + reluBranchFacts .negative + +private def reluLeftSeed : + ProofEmitter.BranchSeed reluSemantics reluLeftInput reluBaseFacts + (reluBranchFact .nonnegative) := + ProofEmitter.BranchSeed.make reluLeftInput (reluBranchFact .nonnegative) + (by rfl) (by rfl) (reluInherit .nonnegative) + +private def reluRightSeed : + ProofEmitter.BranchSeed reluSemantics reluRightInput reluBaseFacts + (reluBranchFact .negative) := + ProofEmitter.BranchSeed.make reluRightInput (reluBranchFact .negative) + (by rfl) (by rfl) (reluInherit .negative) + +private structure ReluRun where + session : PolicySession.Session Bound + registry : ProofRegistry.Registry reluSemantics Name + reached : TargetRun.Reached Bound + +private def reluRunChild? (side : Bound) (input : CheckerInput Bound) + (scope : Propagator.Policy.ScopeId) : Option ReluRun := do + let key := if side == .nonnegative then reluNonnegativeKey else reluNegativeKey + let result ← reluRunWith? reluPackages input (reluRulePolicy key) scope + let .target reached := result.stop | none + let .ok registry := ProofRegistry.build result.session.registry reluProofPackages + | none + some { session := result.session, registry, reached } + +#guard + reluPrepared?.any fun lifted => + let children := lifted.down + children.leftScope == ({ index := 1 } : Propagator.Policy.ScopeId) && + children.rightScope == ({ index := 2 } : Propagator.Policy.ScopeId) && + children.left.baseProgram == reluLeftInput.baseProgram && + children.left.initialFacts == reluLeftInput.initialFacts && + children.left.target == reluLeftInput.target && + children.right.baseProgram == reluRightInput.baseProgram && + children.right.initialFacts == reluRightInput.initialFacts && + children.right.target == reluRightInput.target + +private def reluTraceUses? (side : Bound) (input : CheckerInput Bound) + (scope : Propagator.Policy.ScopeId) : Bool := + match reluRunChild? side input scope with + | none => false + | some run => + match Frontend.trace? run.session.state.engine run.session.arena with + | some trace => + match trace.events with + | [.rule step] => + step.assumptions == [reluBranchFact side] && + step.event.fact == .nonnegative && + step.entry.replayKey == + (if side == .nonnegative then reluNonnegativeSchema.key + else reluNegativeSchema.key) + | _ => false + | none => false + +#guard reluTraceUses? .nonnegative reluLeftInput { index := 1 } +#guard reluTraceUses? .negative reluRightInput { index := 2 } + +private def reluRejectsUnsplit? (key : RuleKey) : Bool := + reluRunWith? reluPackages reluInput (reluRulePolicy key) |>.any fun result => + (match result.stop with | .target _ => false | _ => true) && + result.session.state.engine.facts == #[.all, .all] && + result.session.state.engine.history.isEmpty + +#guard reluRejectsUnsplit? reluNonnegativeKey +#guard reluRejectsUnsplit? reluNegativeKey + +private theorem reluBranchWithin (side : Bound) : + FactsWithin reluProgram (reluBranchFacts side) := by + intro fact member + simp only [reluBranchFacts, reluBranchFact, reluBaseFacts, List.mem_cons, + List.not_mem_nil, or_false] at member + rcases member with rfl | rfl | rfl <;> simp [reluProgram, node] + +private def reluSeedAssumed (graph : Program) (base : List (NodeFact Bound)) + (index : Nat) (fact : NodeFact Bound) (found : base[index]? = some fact) : + Evidence (reluSemantics.Entails graph base fact) := + ProofEmitter.assumedAt graph base index fact found + +private def reluContext (input facts within : Expr) + (factValues : List (NodeFact Bound)) : ProofFrontend.Context Bound Name := + { encoder := boundEncoder + resolveSchema := pure + semantics := mkConst ``reluSemantics + domain := mkConst ``reluBoundSchema + laws := mkConst ``reluLaws + stableLaw := mkConst ``reluStableLaw + input + assumed := ``reluSeedAssumed + baseFacts := factValues + baseFactsTerm := facts + baseProgram := reluProgram + baseProgramTerm := mkConst ``reluProgram + basePrefix := mkConst ``reluBasePrefix + baseWithin := within + initialExtension := mkConst ``reluInitialExtension + finalPrefix := mkConst ``reluBasePrefix + sameOperations := mkConst ``reluSameOperations + top := reluBoundSchema.top } + +private def reluLeftContext : ProofFrontend.Context Bound Name := + reluContext (mkConst ``reluLeftInput) (mkConst ``reluLeftFacts) + (mkApp (mkConst ``reluBranchWithin) (mkConst ``Bound.nonnegative)) + reluLeftFacts + +private def reluRightContext : ProofFrontend.Context Bound Name := + reluContext (mkConst ``reluRightInput) (mkConst ``reluRightFacts) + (mkApp (mkConst ``reluBranchWithin) (mkConst ``Bound.negative)) + reluRightFacts + +private def reluParent : Evidence + (reluSemantics.Entails reluProgram reluBaseFacts (reluBranchFact .all)) := + ProofEmitter.assumed (by simp [reluBaseFacts, reluBranchFact, node]) + +private meta def emitReluChild (context : ProofFrontend.Context Bound Name) + (side : Bound) (input : CheckerInput Bound) + (scope : Propagator.Policy.ScopeId) (seed : Expr) : MetaM Expr := do + let some run := reluRunChild? side input scope + | throwError "interval_relu_split: child search failed" + let some trace := Frontend.trace? run.session.state.engine run.session.arena + | throwError "interval_relu_split: child chronology quotation failed" + let state ← ProofFrontend.emitBranch context input seed trace.program + trace.events run.registry.emit + ProofFrontend.closeTarget context state run.reached.seen run.reached.fact input.target + +private meta def emitReluSplit : MetaM Expr := do + let some lifted := reluPrepared? + | throwError "interval_relu_split: branch preparation failed" + let children := lifted.down + let left ← emitReluChild reluLeftContext .nonnegative children.left + children.leftScope (mkConst ``reluLeftSeed) + let right ← emitReluChild reluRightContext .negative children.right + children.rightScope (mkConst ``reluRightSeed) + let result ← + mkAppM ``ProofEmitter.replaySplit + #[mkConst ``reluSplitSchema, mkConst ``reluProgram, + mkConst ``reluBaseFacts, ← boundEncoder.nodeId (node 0), + ← boundEncoder.fact .all, mkConst ``Unit.unit, + ← boundEncoder.fact .nonnegative, ← boundEncoder.fact .negative, + ← boundEncoder.nodeFact reluInput.target, + mkConst ``reluParent, left, right] + ProofFrontend.replayResult result + +/-- The emitted term contains both live child replays and the checked generic +split join. Assigning that term to this declaration makes the ordinary kernel, +not the Meta evaluator, validate the complete proof. -/ +private def reluJoined : Evidence + (reluSemantics.Entails reluProgram reluBaseFacts reluInput.target) := by + run_tac + let goal ← getMainGoal + goal.assign (← emitReluSplit) + +/-- A genuinely branch-dependent arbitrary-function vertical: neither ReLU +propagator fires before the zero split, and each child proof consumes its own +strictly narrower source fact before the generic join closes the theorem. -/ +theorem tacticReluSplit (x : ℝ) : 0 ≤ max x 0 := + closeRelu x reluJoined + +set_option linter.unusedTactic false in +example : True := by + run_tac + let checkMutation (context : ProofFrontend.Context Bound Name) + (side wrong : Bound) (input : CheckerInput Bound) + (scope : Propagator.Policy.ScopeId) (seed : Expr) : MetaM Unit := do + let some run := reluRunChild? side input scope + | throwError "interval_relu_split mutation: child search failed" + let some trace := Frontend.trace? run.session.state.engine run.session.arena + | throwError "interval_relu_split mutation: trace missing" + let [.rule step] := trace.events + | throwError "interval_relu_split mutation: wrong trace shape" + let mutated : RuleStep Bound := + { step with assumptions := [reluBranchFact wrong] } + if (← observing? <| ProofFrontend.emitBranch context input seed trace.program + [.rule mutated] run.registry.emit).isSome then + throwError + "interval_relu_split mutation: opposite split assumption was accepted" + checkMutation reluLeftContext .nonnegative .negative reluLeftInput + { index := 1 } (mkConst ``reluLeftSeed) + checkMutation reluRightContext .negative .nonnegative reluRightInput + { index := 2 } (mkConst ``reluRightSeed) + trivial + end Hex.IntervalMathlib.ExpSignConformance diff --git a/progress/20260811T153755Z.md b/progress/20260811T153755Z.md new file mode 100644 index 000000000..11654788f --- /dev/null +++ b/progress/20260811T153755Z.md @@ -0,0 +1,32 @@ +# Accomplished + +- Added a conformance-local max-zero/ReLU operation with two side-specific + runtime handlers and matching semantic replay schemas. +- Ran the real checked branch-start transition, then started and replayed both + exact child sessions through the generic proof frontend. +- Installed the emitted two-child split proof in an ordinary kernel-checked + declaration and derived `0 ≤ max x 0` from it. +- Added guards showing that neither rule fires from the unsplit top fact, that + each live trace records its exact split assumption, and that substituting the + opposite sibling assumption makes proof emission fail. +- Kept the branch manager, proof frontend, and split join unchanged and free of + function-specific cases. +- Built `HexIntervalMathlib.ExpSignConformance` and ran the copyright, + line-count, dependency-DAG, trust-surface, phase-four, factor-freshness, and + diff checks successfully. + +# Current frontier + +The smallest branch-dependent arbitrary-function vertical is executable and +kernel checked. Its experimental ReLU package currently lives beside the +exponential conformance fixture to avoid changing the public module graph. + +# Next step + +Review whether the ReLU package should remain a compact conformance fixture or +be promoted into separate Mathlib-free runtime and Mathlib semantic modules +before opening a PR. + +# Blockers + +None. diff --git a/progress/20260811T155115Z.md b/progress/20260811T155115Z.md new file mode 100644 index 000000000..31bec5f07 --- /dev/null +++ b/progress/20260811T155115Z.md @@ -0,0 +1,25 @@ +# Accomplished + +- Rebased the assumption-dependent max-zero/ReLU vertical onto the generic + proof-refutation stack without changing the branch manager or proof frontend. +- Preserved both live side-specific propagators, exact child chronology replay, + swapped-assumption rejection, and the ordinary kernel theorem + `0 ≤ max x 0`. +- Updated the SPEC to distinguish this useful two-proof vertical from the + separate mixed target/refutation join. + +# Current frontier + +The framework now has two complementary branch canaries: one joins a target +leaf with a proof-refuted leaf, and one joins two non-contradictory proofs which +genuinely depend on different function-package rules and split assumptions. + +# Next step + +After the branch-start freshness repair is reconciled, promote the reusable +max-zero runtime and semantic pieces out of the conformance fixture if the +review confirms that the package boundary is the right one. + +# Blockers + +None. diff --git a/progress/20260811T165120Z.md b/progress/20260811T165120Z.md new file mode 100644 index 000000000..61358aa90 --- /dev/null +++ b/progress/20260811T165120Z.md @@ -0,0 +1,28 @@ +# Accomplished + +- Restacked the useful branch-dependent max-zero/ReLU vertical onto the exact + repaired refutation-frontend head + `c3023fbffd9e2a43a374e0d7f1bcc061c7d22c67`. +- Preserved the two live child runs: the nonnegative rule consumes only the + left split fact, and the negative rule consumes only the right split fact. +- Preserved the unsplit-top rejection guards, exact child-trace checks, + opposite-assumption mutation guards, generic branch seeding and replay, and + the ordinary kernel theorem `tacticReluSplit`. +- Built the focused conformance targets and passed source, dependency-DAG, + trust-surface, phase-four, factor-freshness, banned-construct, and diff + checks. + +# Current frontier + +The useful two-proof ReLU canary is reconciled with the repaired split and +proof-refutation stack. A fresh isolated review and exact-head CI remain the +merge gates. + +# Next step + +Obtain the independent exact-head review, verify any findings against the +source, and monitor the superseding CI run without merging the stack. + +# Blockers + +None. From cb90c561b5275dc05b9a4cc4455e596c145180cb Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Aug 2026 17:41:14 +0000 Subject: [PATCH 2/8] docs(interval): state ReLU evidence precisely; progress 20260811T165120Z --- HexInterval/SPEC/hex-interval.md | 27 +++++++++++++++------------ progress/20260811T165120Z.md | 9 +++++---- 2 files changed, 20 insertions(+), 16 deletions(-) diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index a7cacd6b6..3f57ace85 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1714,18 +1714,21 @@ first two-sided live execution and proof join, but exponential nonnegativity is unconditional: neither child target proof currently needs its split assumption. The mixed target/refutation join does consume the two incompatible output assumptions. A separate conformance-local max-zero/ReLU package now -supplies the first useful non-contradictory branch-dependent vertical. Its -nonnegative rule proves `max x 0 = x` only from the left split fact; its strict -negative rule proves `max x 0 = 0` only from the right split fact. Both child -sessions retain one ordinary rule event with the exact side fact as an input, -the unchanged generic frontend replays them, and `replaySplit` produces 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 companion. Remaining -acceptance tests include a nested split, a child-local instantiation, a -sibling-reference attack, a non-interior repeated split, and fuel exhaustion -with no theorem emitted. +uses deliberately conditional rules to supply the first useful +non-contradictory branch-dependent vertical, even though its final theorem is +itself unconditional. The nonnegative-side rule proves the output fact by +rewriting `max x 0` to `x` from the left split fact; the strict-negative rule +proves the same output fact by rewriting `max x 0` to `0` from the right split +fact. Both child sessions retain one ordinary rule event with the exact side +fact as an input, the unchanged generic frontend 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 +companion. Remaining acceptance tests include 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 diff --git a/progress/20260811T165120Z.md b/progress/20260811T165120Z.md index 61358aa90..2a3cec8b7 100644 --- a/progress/20260811T165120Z.md +++ b/progress/20260811T165120Z.md @@ -11,17 +11,18 @@ - Built the focused conformance targets and passed source, dependency-DAG, trust-surface, phase-four, factor-freshness, banned-construct, and diff checks. +- Tightened the SPEC to say exactly what the two conditional rules prove, to + distinguish the generic split entailment from final theorem specialization, + and to state explicitly that the canary's conclusion is unconditional. # Current frontier The useful two-proof ReLU canary is reconciled with the repaired split and -proof-refutation stack. A fresh isolated review and exact-head CI remain the -merge gates. +proof-refutation stack. Exact-head CI remains the merge gate. # Next step -Obtain the independent exact-head review, verify any findings against the -source, and monitor the superseding CI run without merging the stack. +Monitor the superseding exact-head CI run without merging the stack. # Blockers From 5d99d3dfaab41f033b7c97e6e47ee765682571da Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 16:17:42 +0000 Subject: [PATCH 3/8] Pin ReLU branch trace fidelity --- .../ExpSignConformance.lean | 47 +++++++++++++++---- progress/20260814T161713Z.md | 31 ++++++++++++ 2 files changed, 69 insertions(+), 9 deletions(-) create mode 100644 progress/20260814T161713Z.md diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean index 20dcaed1b..ab6f2b8d7 100644 --- a/conformance/HexIntervalMathlib/ExpSignConformance.lean +++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean @@ -1770,7 +1770,7 @@ private def reluPrepared? : match result.stop with | .split plan => match BranchStart.prepare branchLimits - (BranchStart.State.start { index := 0 }) 0 result.session plan + (BranchStart.State.start result.session) result.session plan reluInput.target signSplitter with | .ok (_, children) => some (ULift.up children) | .error _ => none @@ -1847,14 +1847,11 @@ private def reluRunChild? (side : Bound) (input : CheckerInput Bound) #guard reluPrepared?.any fun lifted => let children := lifted.down - children.leftScope == ({ index := 1 } : Propagator.Policy.ScopeId) && + children.depth == 1 && sameChecker children.parent reluInput && + children.leftScope == ({ index := 1 } : Propagator.Policy.ScopeId) && children.rightScope == ({ index := 2 } : Propagator.Policy.ScopeId) && - children.left.baseProgram == reluLeftInput.baseProgram && - children.left.initialFacts == reluLeftInput.initialFacts && - children.left.target == reluLeftInput.target && - children.right.baseProgram == reluRightInput.baseProgram && - children.right.initialFacts == reluRightInput.initialFacts && - children.right.target == reluRightInput.target + sameChecker children.left reluLeftInput && + sameChecker children.right reluRightInput private def reluTraceUses? (side : Bound) (input : CheckerInput Bound) (scope : Propagator.Policy.ScopeId) : Bool := @@ -1865,8 +1862,18 @@ private def reluTraceUses? (side : Bound) (input : CheckerInput Bound) | some trace => match trace.events with | [.rule step] => - step.assumptions == [reluBranchFact side] && + trace.program == input.baseProgram && + run.reached.seen == + ({ node := node 1, version := 1 } : SeenVersion) && + run.reached.fact == .nonnegative && + run.session.state.engine.facts == #[side, .nonnegative] && + run.session.state.engine.versions == #[0, 1] && + step.assumptions == [reluBranchFact side] && + step.event.programVersion == 0 && step.event.node == node 1 && + step.event.previous == + ({ node := node 1, version := 0 } : SeenVersion) && step.event.fact == .nonnegative && + step.event.version == 1 && step.previous == .all && step.entry.replayKey == (if side == .nonnegative then reluNonnegativeSchema.key else reluNegativeSchema.key) @@ -1939,6 +1946,22 @@ private meta def emitReluChild (context : ProofFrontend.Context Bound Name) | throwError "interval_relu_split: child search failed" let some trace := Frontend.trace? run.session.state.engine run.session.arena | throwError "interval_relu_split: child chronology quotation failed" + let [.rule step] := trace.events + | throwError "interval_relu_split: child trace is not exactly one rule" + let expectedKey := + if side == .nonnegative then reluNonnegativeSchema.key + else reluNegativeSchema.key + unless trace.program == input.baseProgram && + run.reached.seen == ({ node := node 1, version := 1 } : SeenVersion) && + run.reached.fact == .nonnegative && + run.session.state.engine.facts == #[side, .nonnegative] && + run.session.state.engine.versions == #[0, 1] && + step.assumptions == [reluBranchFact side] && + step.event.programVersion == 0 && step.event.node == node 1 && + step.event.previous == ({ node := node 1, version := 0 } : SeenVersion) && + step.event.fact == .nonnegative && step.event.version == 1 && + step.previous == .all && step.entry.replayKey == expectedKey do + throwError "interval_relu_split: child result or quoted rule trace drifted" let state ← ProofFrontend.emitBranch context input seed trace.program trace.events run.registry.emit ProofFrontend.closeTarget context state run.reached.seen run.reached.fact input.target @@ -1976,6 +1999,12 @@ strictly narrower source fact before the generic join closes the theorem. -/ theorem tacticReluSplit (x : ℝ) : 0 ≤ max x 0 := closeRelu x reluJoined +/-- +info: 'Hex.IntervalMathlib.ExpSignConformance.tacticReluSplit' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms tacticReluSplit + set_option linter.unusedTactic false in example : True := by run_tac diff --git a/progress/20260814T161713Z.md b/progress/20260814T161713Z.md new file mode 100644 index 000000000..b4a7ccc3e --- /dev/null +++ b/progress/20260814T161713Z.md @@ -0,0 +1,31 @@ +# PR #9223 reconciliation + +## Accomplished + +- Replayed only the conformance-local max-zero/ReLU vertical and its honesty + repair onto exact current `main`, preserving merged #9222 and #9256 content. +- Updated branch preparation to derive its sealed root state from the exact + engine-owned session. +- Verified the premise: the nonnegative schema consumes exactly the left split + fact, the negative schema consumes exactly the right split fact, neither + runtime rule fires from the unsplit top fact, and swapped assumptions fail. +- Strengthened the live canary to pin parent/depth/child inputs/scopes and each + child's complete one-rule chronology, reached version, installed facts, and + package replay key. +- Added a guarded dependency report for the ordinary `tacticReluSplit` + theorem. + +## Current frontier + +- The generic branch/frontend framework now proves a useful arbitrary-function + example whose two non-contradictory child proofs genuinely depend on distinct + split assumptions; promotion beyond conformance remains an open choice. + +## Next step + +- Run focused/static checks, push and retarget the PR, then obtain fresh + exact-head review and CI evidence. + +## Blockers + +- None. From 59c45aa610d0fc346f0fd12a57a3d1fd19fdff97 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 16:32:06 +0000 Subject: [PATCH 4/8] docs(interval): clarify ReLU branch canary scope --- HexInterval/SPEC/hex-interval.md | 20 +++++++++++--------- progress/20260814T161713Z.md | 10 +++++++--- 2 files changed, 18 insertions(+), 12 deletions(-) diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 3f57ace85..328cc002c 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1714,19 +1714,21 @@ first two-sided live execution and proof join, but exponential nonnegativity is unconditional: neither child target proof currently needs its split assumption. The mixed target/refutation join does consume the two incompatible output assumptions. A separate conformance-local max-zero/ReLU package now -uses deliberately conditional rules to supply the first useful -non-contradictory branch-dependent vertical, even though its final theorem is -itself unconditional. The nonnegative-side rule proves the output fact by -rewriting `max x 0` to `x` from the left split fact; the strict-negative rule -proves the same output fact by rewriting `max x 0` to `0` from the right split -fact. Both child sessions retain one ordinary rule event with the exact side -fact as an input, the unchanged generic frontend replays them, and -`replaySplit` produces the joined entailment evidence. `closeRelu` specializes +uses deliberately conditional rules to supply the first explicit +non-contradictory distinct-assumption plumbing vertical. This conditionality +is a package-test design choice, not a claim that branching is mathematically +necessary for its unconditional final theorem. The nonnegative-side rule +proves the output fact by rewriting `max x 0` to `x` from the left split fact; +the strict-negative rule proves the same output fact by rewriting `max x 0` to +`0` from the right split fact. Both child sessions retain one ordinary rule +event with the exact side fact as an input, the unchanged generic frontend +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 -companion. Remaining acceptance tests include a nested split, a child-local +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. diff --git a/progress/20260814T161713Z.md b/progress/20260814T161713Z.md index b4a7ccc3e..56c326872 100644 --- a/progress/20260814T161713Z.md +++ b/progress/20260814T161713Z.md @@ -14,12 +14,16 @@ package replay key. - Added a guarded dependency report for the ordinary `tacticReluSplit` theorem. +- Clarified that the ReLU rules deliberately test distinct-assumption + plumbing; the unconditional result does not establish that branching is + mathematically necessary, which remains a separate acceptance test. ## Current frontier -- The generic branch/frontend framework now proves a useful arbitrary-function - example whose two non-contradictory child proofs genuinely depend on distinct - split assumptions; promotion beyond conformance remains an open choice. +- The generic branch/frontend framework now proves an arbitrary-function + conformance example whose two non-contradictory child proofs genuinely + consume distinct split assumptions; promotion beyond conformance remains an + open choice. ## Next step From ce5843bbabc7d10878c4bd6361e6f8d58768be1d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 16:43:59 +0000 Subject: [PATCH 5/8] docs(interval): name ReLU conformance honestly --- .../ExpSignConformance.lean | 23 +++++++++++-------- progress/20260814T161713Z.md | 7 +++--- 2 files changed, 17 insertions(+), 13 deletions(-) diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean index ab6f2b8d7..628f38e0e 100644 --- a/conformance/HexIntervalMathlib/ExpSignConformance.lean +++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean @@ -1455,10 +1455,12 @@ example : True := by /-! ## Branch-dependent ReLU propagation Unlike exponential positivity, these two propagators are intentionally -conditional. The nonnegative-side rule proves `max x 0 = x` from `0 <= x`; -the negative-side rule proves `max x 0 = 0` from `x < 0`. The runtime and -proof packages know those two function-specific facts, while branch creation, -branch seeding, chronology replay, and the two-proof join stay generic. -/ +conditional. The nonnegative-side rule proves the output fact by rewriting +with `max x 0 = x` from `0 <= x`; the negative-side rule does so by rewriting +with `max x 0 = 0` from `x < 0`. This conditionality is a package-test design +choice for an unconditional final theorem. The runtime and proof packages +know those two function-specific facts, while branch creation, branch seeding, +chronology replay, and the two-proof join stay generic. -/ private def reluKey : OpKey := { name := "relu-sign.max-zero" } @@ -1993,17 +1995,18 @@ private def reluJoined : Evidence let goal ← getMainGoal goal.assign (← emitReluSplit) -/-- A genuinely branch-dependent arbitrary-function vertical: neither ReLU -propagator fires before the zero split, and each child proof consumes its own -strictly narrower source fact before the generic join closes the theorem. -/ -theorem tacticReluSplit (x : ℝ) : 0 ≤ max x 0 := +/-- An arbitrary-function vertical whose child proofs consume distinct split +assumptions by construction: neither ReLU propagator fires before the zero +split. The final theorem is unconditional; conditionality here tests the +branch proof plumbing rather than mathematical necessity. -/ +theorem reluSplit (x : ℝ) : 0 ≤ max x 0 := closeRelu x reluJoined /-- -info: 'Hex.IntervalMathlib.ExpSignConformance.tacticReluSplit' depends on axioms: [propext, Classical.choice, Quot.sound] +info: 'Hex.IntervalMathlib.ExpSignConformance.reluSplit' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in -#print axioms tacticReluSplit +#print axioms reluSplit set_option linter.unusedTactic false in example : True := by diff --git a/progress/20260814T161713Z.md b/progress/20260814T161713Z.md index 56c326872..5c83935a6 100644 --- a/progress/20260814T161713Z.md +++ b/progress/20260814T161713Z.md @@ -12,11 +12,13 @@ - Strengthened the live canary to pin parent/depth/child inputs/scopes and each child's complete one-rule chronology, reached version, installed facts, and package replay key. -- Added a guarded dependency report for the ordinary `tacticReluSplit` +- Added a guarded dependency report for the ordinary `reluSplit` theorem. - Clarified that the ReLU rules deliberately test distinct-assumption plumbing; the unconditional result does not establish that branching is mathematically necessary, which remains a separate acceptance test. +- Kept the theorem name and docstring honest about the absence of goal-tactic + reification in this conformance vertical. ## Current frontier @@ -27,8 +29,7 @@ ## Next step -- Run focused/static checks, push and retarget the PR, then obtain fresh - exact-head review and CI evidence. +- Await the final exact-head independent review and CI evidence. ## Blockers From 4867280d7c38f67b92987058a059600727b64f01 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 16:52:58 +0000 Subject: [PATCH 6/8] docs(progress): record final ReLU restack --- progress/20260814T161713Z.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/progress/20260814T161713Z.md b/progress/20260814T161713Z.md index 5c83935a6..5dce32549 100644 --- a/progress/20260814T161713Z.md +++ b/progress/20260814T161713Z.md @@ -19,6 +19,9 @@ mathematically necessary, which remains a separate acceptance test. - Kept the theorem name and docstring honest about the absence of goal-tactic reification in this conformance vertical. +- Restacked the byte-identical feature patch onto exact `main` after the PNT + log-table merge, preserving its inventory and fixture; both focused ReLU and + PNT conformance builds and the static checks pass. ## Current frontier From 7481e1ba2b722c9b5efbfda535b532c3c1243b63 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 17:01:40 +0000 Subject: [PATCH 7/8] docs(interval): finish ReLU naming cleanup --- HexInterval/SPEC/hex-interval.md | 5 +++-- progress/20260811T165120Z.md | 6 +++--- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 328cc002c..08bcff5b3 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1722,8 +1722,9 @@ proves the output fact by rewriting `max x 0` to `x` from the left split fact; the strict-negative rule proves the same output fact by rewriting `max x 0` to `0` from the right split fact. Both child sessions retain one ordinary rule event with the exact side fact as an input, the unchanged generic frontend -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 +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 diff --git a/progress/20260811T165120Z.md b/progress/20260811T165120Z.md index 2a3cec8b7..9181a9571 100644 --- a/progress/20260811T165120Z.md +++ b/progress/20260811T165120Z.md @@ -1,13 +1,13 @@ # Accomplished -- Restacked the useful branch-dependent max-zero/ReLU vertical onto the exact +- Restacked the distinct-assumption max-zero/ReLU vertical onto the exact repaired refutation-frontend head `c3023fbffd9e2a43a374e0d7f1bcc061c7d22c67`. - Preserved the two live child runs: the nonnegative rule consumes only the left split fact, and the negative rule consumes only the right split fact. - Preserved the unsplit-top rejection guards, exact child-trace checks, opposite-assumption mutation guards, generic branch seeding and replay, and - the ordinary kernel theorem `tacticReluSplit`. + the ordinary kernel theorem now named `reluSplit`. - Built the focused conformance targets and passed source, dependency-DAG, trust-surface, phase-four, factor-freshness, banned-construct, and diff checks. @@ -17,7 +17,7 @@ # Current frontier -The useful two-proof ReLU canary is reconciled with the repaired split and +The two-proof ReLU canary is reconciled with the repaired split and proof-refutation stack. Exact-head CI remains the merge gate. # Next step From 3077bb04a9f05a7c9058b552b1200691d9377ddf Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Aug 2026 17:34:20 +0000 Subject: [PATCH 8/8] docs(interval): finish ReLU restack polish --- HexInterval/SPEC/hex-interval.md | 6 +++--- progress/20260811T153755Z.md | 4 ++-- progress/20260811T155115Z.md | 2 +- progress/20260811T165120Z.md | 5 ++--- progress/20260814T161713Z.md | 8 +++++--- 5 files changed, 13 insertions(+), 12 deletions(-) diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 08bcff5b3..19e7cd215 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1724,9 +1724,9 @@ the strict-negative rule proves the same output fact by rewriting `max x 0` to event with the exact side fact as an input, the unchanged generic frontend 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 +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 companion. Remaining acceptance tests include a theorem whose proof mathematically requires branching, a nested split, a child-local diff --git a/progress/20260811T153755Z.md b/progress/20260811T153755Z.md index 11654788f..e912f3bb4 100644 --- a/progress/20260811T153755Z.md +++ b/progress/20260811T153755Z.md @@ -17,8 +17,8 @@ # Current frontier -The smallest branch-dependent arbitrary-function vertical is executable and -kernel checked. Its experimental ReLU package currently lives beside the +The smallest distinct-assumption arbitrary-function vertical is executable +and kernel checked. Its experimental ReLU package currently lives beside the exponential conformance fixture to avoid changing the public module graph. # Next step diff --git a/progress/20260811T155115Z.md b/progress/20260811T155115Z.md index 31bec5f07..621fef10c 100644 --- a/progress/20260811T155115Z.md +++ b/progress/20260811T155115Z.md @@ -5,7 +5,7 @@ - Preserved both live side-specific propagators, exact child chronology replay, swapped-assumption rejection, and the ordinary kernel theorem `0 ≤ max x 0`. -- Updated the SPEC to distinguish this useful two-proof vertical from the +- Updated the SPEC to distinguish this distinct-assumption vertical from the separate mixed target/refutation join. # Current frontier diff --git a/progress/20260811T165120Z.md b/progress/20260811T165120Z.md index 9181a9571..45664da4f 100644 --- a/progress/20260811T165120Z.md +++ b/progress/20260811T165120Z.md @@ -1,8 +1,7 @@ # Accomplished -- Restacked the distinct-assumption max-zero/ReLU vertical onto the exact - repaired refutation-frontend head - `c3023fbffd9e2a43a374e0d7f1bcc061c7d22c67`. +- Restacked the distinct-assumption max-zero/ReLU vertical onto the repaired + refutation frontend. - Preserved the two live child runs: the nonnegative rule consumes only the left split fact, and the negative rule consumes only the right split fact. - Preserved the unsplit-top rejection guards, exact child-trace checks, diff --git a/progress/20260814T161713Z.md b/progress/20260814T161713Z.md index 5dce32549..d2f145994 100644 --- a/progress/20260814T161713Z.md +++ b/progress/20260814T161713Z.md @@ -19,9 +19,11 @@ mathematically necessary, which remains a separate acceptance test. - Kept the theorem name and docstring honest about the absence of goal-tactic reification in this conformance vertical. -- Restacked the byte-identical feature patch onto exact `main` after the PNT - log-table merge, preserving its inventory and fixture; both focused ReLU and - PNT conformance builds and the static checks pass. +- Restacked the byte-identical Lean feature patch onto exact `main` + `4cbf00eac03c1e47b053218bad7c123623b5511b`, preserving the PNT log, + Machin, and endpoint-sine additions. +- Built the ReLU, PNT-log, Machin, and endpoint-sine conformance targets and + passed the source, trust, freshness, inventory, and banned-proof checks. ## Current frontier