diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md index 62a6ae254..19e7cd215 100644 --- a/HexInterval/SPEC/hex-interval.md +++ b/HexInterval/SPEC/hex-interval.md @@ -1713,11 +1713,25 @@ 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 -sibling-reference attack, a non-interior repeated split, and fuel exhaustion -with no theorem emitted. +output assumptions. A separate conformance-local max-zero/ReLU package now +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 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-producing frontend diff --git a/conformance/HexIntervalMathlib/ExpSignConformance.lean b/conformance/HexIntervalMathlib/ExpSignConformance.lean index 26325cc56..628f38e0e 100644 --- a/conformance/HexIntervalMathlib/ExpSignConformance.lean +++ b/conformance/HexIntervalMathlib/ExpSignConformance.lean @@ -1452,4 +1452,584 @@ 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 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" } + +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 result.session) 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.depth == 1 && sameChecker children.parent reluInput && + children.leftScope == ({ index := 1 } : Propagator.Policy.ScopeId) && + children.rightScope == ({ index := 2 } : Propagator.Policy.ScopeId) && + sameChecker children.left reluLeftInput && + sameChecker children.right reluRightInput + +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] => + 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) + | _ => 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 [.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 + +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) + +/-- 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.reluSplit' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in +#print axioms reluSplit + +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..e912f3bb4 --- /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 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 + +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..621fef10c --- /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 distinct-assumption 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..45664da4f --- /dev/null +++ b/progress/20260811T165120Z.md @@ -0,0 +1,28 @@ +# Accomplished + +- 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, + opposite-assumption mutation guards, generic branch seeding and replay, and + 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. +- 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 two-proof ReLU canary is reconciled with the repaired split and +proof-refutation stack. Exact-head CI remains the merge gate. + +# Next step + +Monitor the superseding exact-head CI run without merging the stack. + +# Blockers + +None. diff --git a/progress/20260814T161713Z.md b/progress/20260814T161713Z.md new file mode 100644 index 000000000..d2f145994 --- /dev/null +++ b/progress/20260814T161713Z.md @@ -0,0 +1,41 @@ +# 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 `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. +- 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 + +- 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 + +- Await the final exact-head independent review and CI evidence. + +## Blockers + +- None.