Add proof-producing contradiction leaves

HexInterval/Experiment/ProofEmitter.lean

@@ -19,11 +19,12 @@ opaque search, and a proof recovered from the evaluator would put that
 evaluator in the trusted base.
 
 The tactic boundary instead quotes the search output as plain data.  This
-module provides transparent replay for the three proof-producing event shapes
-a tactic must quote: expression instantiation, a rule fact, and equality
-transport.  Each transition selects a package-owned theorem schema supplied
-by the caller, checks its replay address and the event's structural links, and
-composes the resulting theorem with generic semantic lemmas.
+module provides transparent replay for the proof-producing transitions a
+tactic must quote: expression instantiation, rule facts, equality transport,
+branch joins, and contradiction leaves.  Each transition selects a
+package-owned theorem schema supplied by the caller, checks its replay address
+and structural links, and composes the resulting theorem with generic semantic
+lemmas.
 
 The schemas remain abstract: neither these quote types nor their replay
 functions enumerate operations or supported mathematical functions.  A
@@ -501,6 +502,48 @@ def replaySplit {Fact Cut : Type} {semantics : Semantics Fact}
   let cover <- schema.proveCover program node parent cut left right
   pure (installSplit cover parentSound leftSound rightSound)
 
+/-! ## Proof-producing contradiction leaves -/
+
+/-- Package-owned proof boundary for one contradictory fact.
+
+The runtime engine may mark a branch contradictory after installing a bottom
+fact, but that flag is search state rather than evidence.  A domain companion
+must independently prove that the exact established fact is impossible under
+the program semantics. -/
+structure RefuteSchema (semantics : Semantics Fact) where
+  proveFalse :
+    (program : Program) -> (node : NodeId) -> (fact : Fact) ->
+      Option
+        (Evidence
+          (forall valuation, semantics.models program valuation ->
+            semantics.holds program valuation { node, fact } -> False))
+
+/-- Eliminate one checked impossible fact into an arbitrary branch target. -/
+def installRefute {Fact : Type} {semantics : Semantics Fact}
+    {program : Program} {base : List (NodeFact Fact)}
+    {fact target : NodeFact Fact}
+    (impossible :
+      Evidence
+        (forall valuation, semantics.models program valuation ->
+          semantics.holds program valuation fact -> False))
+    (factSound : Evidence (semantics.Entails program base fact)) :
+    Evidence (semantics.Entails program base target) :=
+  { proof := by
+      intro valuation model baseHolds
+      exact False.elim
+        (impossible.proof valuation model
+          (factSound.proof valuation model baseHolds)) }
+
+/-- Transparently replay one contradiction leaf from the exact established
+fact.  No runtime contradiction flag enters the returned theorem. -/
+def replayRefute {Fact : Type} {semantics : Semantics Fact}
+    (schema : RefuteSchema semantics) (program : Program)
+    (base : List (NodeFact Fact)) (fact target : NodeFact Fact)
+    (factSound : Evidence (semantics.Entails program base fact)) :
+    Option (Evidence (semantics.Entails program base target)) := do
+  let impossible <- schema.proveFalse program fact.node fact.fact
+  pure (installRefute impossible factSound)
+
 /-! ## Provenance-safe branch roots -/
 
 /-- An established parent fact remains established after adding one child

HexInterval/SPEC/hex-interval.md

@@ -1643,20 +1643,38 @@ old target back. Nodes, equality edges, payloads, and positive fact versions
 created below one child are scoped to that child and cannot be resolved by its
 sibling. Parent program nodes and proof terms may be shared structurally.
 
-A runtime contradiction flag is also not a closed child. The proof layer needs
-a domain-owned refutation schema which turns an exact established bottom or
-inconsistent-bound fact into `False`; generic elimination can then produce the
-branch target. Until that schema exists, a contradictory child is useful for
-search diagnostics but cannot participate in a completed join. An unexplored,
-fuel-limited, resource-limited, incomplete, or merely saturated child likewise
-does not close the parent target.
+A runtime contradiction flag is also not a closed child. The generic
+`ProofEmitter.RefuteSchema` now requires a domain companion to turn one exact
+established bottom or inconsistent fact into `False`; `replayRefute` then uses
+ordinary elimination to produce the branch target. The real exponential
+adapter supplies the first `.empty` schema, and its conformance theorem closes
+an arbitrary target from the exact bottom assumption while rejecting `.all`
+by reduction. The conclusion is necessarily ex falso because the canary base
+contains the bottom fact; the conformance obligations are successful
+transparent replay, rejection of the satisfiable `.all` fact, and the guarded
+kernel-dependency report. No engine flag or evaluator result enters that
+theorem.
+Connecting a retained contradictory fact and its emitted evidence to this
+schema inside the tree frontend remains open. An unexplored, fuel-limited,
+resource-limited, incomplete, or merely saturated child likewise does not
+close the parent target.
+
+The later proof-plan sketch represents an endpoint contradiction by two
+`FactId`s, whereas `replayRefute` deliberately consumes one exact established
+fact. Its frontend lowering must therefore either resolve an already-installed
+contradictory meet fact or combine the two retained proofs through the domain's
+`FactDomainSchema.proveMeet` theorem before invoking the refutation schema.
+That lowering must first check that both identifiers name facts at the same
+node. The two-proof bridge remains open; it is not a capability of the current
+single-fact conformance canary.
 
 The first branch-start layer also rebinds each completed child result to the
 exact prepared base program and initial fact array, then rechecks the retained
 target fact and version. Its ordinary two-target closure gate rejects a stopped,
 saturated, fuel-limited, malformed, or wrong-input child. It classifies a
 runtime contradiction separately but deliberately refuses to treat that flag
-as proof closure; the refutation schema described above must land first.
+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

HexIntervalMathlib/Experiment/ExpSign.lean

@@ -88,6 +88,20 @@ def signSplit : SplitSchema semantics Unit where
     else
       none
 
+/-- The exact bottom fact is semantically impossible over `Real`.  Runtime
+contradiction detection is deliberately absent from this proof schema. -/
+def emptyRefute : RefuteSchema semantics where
+  proveFalse := fun _ _ fact =>
+    if shape : fact = .empty then
+      some
+        { proof := by
+            subst fact
+            intro valuation _ impossible
+            change False at impossible
+            exact impossible }
+    else
+      none
+
 theorem expEntails (graph : Program) (assumptions : List (NodeFact Bound))
     (output : NodeId) (instruction : Node) (input : NodeId)
     (found : graph.node? output = some instruction)

conformance/HexIntervalMathlib/RefuteConformance.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+import HexIntervalMathlib.Experiment.ExpSign
+
+/-!
+# Proof-producing contradiction conformance
+
+An engine contradiction flag is not evidence. This canary closes an arbitrary
+target only from an ordinary proof of the exact bottom fact and a package-owned
+semantic refutation of that fact.
+-/
+
+namespace Hex.IntervalMathlib.RefuteConformance
+
+open Hex.Interval.Experiment
+open SemanticReplay ProofEmitter ExpSign
+
+private def bottom : NodeFact Bound :=
+  { node := node 0, fact := .empty }
+
+private def childBase : List (NodeFact Bound) :=
+  bottom :: baseFacts
+
+private def bottomSound : Evidence
+    (semantics.Entails program childBase bottom) :=
+  assumeSplit program baseFacts bottom
+
+private def refuted? : Option
+    (Evidence (semantics.Entails program childBase checkerInput.target)) :=
+  replayRefute emptyRefute program childBase bottom checkerInput.target
+    bottomSound
+
+/-- Transparent refutation replay constructs the expected ordinary kernel
+theorem; the proposition itself is ex falso because `childBase` contains the
+bottom fact. The reduction and guarded dependency report below are the
+conformance obligations, and no evaluator or runtime flag occurs in the
+declaration. -/
+theorem closesTarget :
+    semantics.Entails program childBase checkerInput.target :=
+  proofOfReplay refuted? (by rfl)
+
+/--
+info: 'Hex.IntervalMathlib.RefuteConformance.closesTarget' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs in
+#print axioms closesTarget
+
+private def top : NodeFact Bound :=
+  { node := node 0, fact := .all }
+
+private def topSound : Evidence
+    (semantics.Entails program baseFacts top) :=
+  assumed (by simp [baseFacts, top, node])
+
+/-- Pin the schema's reduction gate: the real adapter rejects a non-bottom
+fact instead of constructing refutation evidence. -/
+example :
+    replayRefute emptyRefute program baseFacts top checkerInput.target
+      topSound = none := by
+  rfl
+
+/-- The negative gate reflects real semantics rather than an empty model:
+`.all` holds in the concrete exponential model and therefore cannot support a
+valid refutation schema. -/
+example :
+    ¬ (∀ valuation, semantics.models program valuation →
+      semantics.holds program valuation top → False) := by
+  intro impossible
+  exact impossible (valuation (0 : ℝ)) (valuationModels 0) (by
+    change Contains .all (valuation (0 : ℝ) (node 0))
+    trivial)
+
+end Hex.IntervalMathlib.RefuteConformance

lakefile.lean

@@ -390,7 +390,7 @@ lean_lib HexRCFProofProbeScientific where
 -- `*_emit_fixtures` exes below, carrying `srcDir := "conformance"`.
 lean_lib HexConformance where
   srcDir := "conformance"
-  globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.ScopeConformance, `HexInterval.StructuralMatcherConformance, `HexInterval.MatcherSchedulerConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexInterval.PolicySessionConformance, `HexInterval.PolicyFunctionConformance, `HexInterval.SemanticReplayConformance, `HexInterval.ChronologicalReplayConformance, `HexInterval.GenericInstanceReconstructionConformance, `HexInterval.ProofEmitterConformance, `HexInterval.TraceReplayConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexMvPolyFixtures, `HexMvPoly.Conformance, `HexMvPolyMathlib.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one
+  globs := #[`HexArith.Conformance, `HexArith.CrossCheck, `HexBerlekamp.Conformance, `HexBerlekampZassenhaus.Conformance, `HexBerlekampZassenhaus.CrossCheck, `HexConway.Conformance, `HexGF2.Conformance, `HexGF2.CrossCheck, `HexGF2.FastCheck, `HexGFq.Conformance, `HexGFq.CrossCheck, `HexGFqField.Conformance, `HexGFqRing.Conformance, `HexGramSchmidt.Conformance, `HexHensel.Conformance, `HexHensel.CrossCheck, `HexInterval.Conformance, `HexInterval.CenterConformance, `HexInterval.ScaleConformance, `HexInterval.PropagatorConformance, `HexInterval.ScopeConformance, `HexInterval.StructuralMatcherConformance, `HexInterval.MatcherSchedulerConformance, `HexInterval.StructureViewConformance, `HexInterval.PolicyConformance, `HexInterval.PolicyFrontierConformance, `HexInterval.PolicyDriverConformance, `HexInterval.PackageRegistryConformance, `HexInterval.DyadicIntervalConformance, `HexInterval.DyadicRulesConformance, `HexInterval.PayloadArenaConformance, `HexInterval.PayloadSessionConformance, `HexInterval.PolicySessionConformance, `HexInterval.PolicyFunctionConformance, `HexInterval.SemanticReplayConformance, `HexInterval.ChronologicalReplayConformance, `HexInterval.GenericInstanceReconstructionConformance, `HexInterval.ProofEmitterConformance, `HexInterval.TraceReplayConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.RefuteConformance, `HexLLL.Conformance, `HexMatrix.Conformance, `HexMvPolyFixtures, `HexMvPoly.Conformance, `HexMvPolyMathlib.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexNumberField.Conformance, `HexNumberFieldTower.Conformance, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRCF.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexResultant.Conformance, `HexRoots.Conformance].map Glob.one
 
 -- Public umbrellas intentionally contain only the supported API. Executable
 -- examples and regression tests are compiled through this separate target so

progress/20260811T154500Z.md

@@ -0,0 +1,23 @@
+# Accomplished
+
+- Added a generic proof-side refutation schema for an exact established fact.
+- Added transparent contradiction elimination which produces an arbitrary
+  branch target without consulting runtime contradiction state.
+- Added the first real-domain adapter for the exponential fact lattice's
+  `.empty` fact.
+- Added an ordinary kernel theorem closing the target from exact bottom
+  evidence and a reduction test rejecting the non-bottom `.all` fact.
+
+# Current frontier
+
+Contradiction leaves now have a sound proof combinator. The tree frontend does
+not yet resolve the retained bottom fact and invoke this schema automatically.
+
+# Next step
+
+Thread package-owned refutation handles through the proof registry and make the
+branch frontend join one target child with one proof-refuted child.
+
+# Blockers
+
+None.

progress/20260811T160743Z.md

@@ -0,0 +1,24 @@
+# Accomplished
+
+- Rebased the contradiction-leaf proof layer onto repaired branch runtime
+  commit `be15a9b1d2026a879c1bf713c86a4fda56633787`.
+- Verified that the real bottom-refutation schema composes with the inherited
+  authenticated branch-start and split proof-registry package changes.
+- Built both refutation and live exponential branch conformance targets and
+  reran trust-surface, phase, DAG, source-lint, and proof-only freshness checks.
+
+# Current frontier
+
+The stacked refutation layer now sits directly on the authenticated branch
+runtime and preserves the split-enabled proof registry's explicit empty
+package. Contradiction evidence is still exposed as a generic transparent
+combinator rather than wired into automatic tree closure.
+
+# Next step
+
+Thread package-owned refutation handles through the proof registry and make the
+branch frontend join one target child with one proof-refuted child.
+
+# Blockers
+
+None.

progress/20260811T165549Z.md

@@ -0,0 +1,24 @@
+# Accomplished
+
+- Reconciled proof-producing contradiction closure with the repaired branch
+  runtime and live split stack.
+- Preserved the exact established-fact lookup and domain-owned refutation
+  schema; runtime contradiction state still never enters kernel evidence.
+- Updated the proof-only Lake exemption to the exact reconciled refutation
+  registration blob while retaining current factorization exemptions.
+
+# Current frontier
+
+A branch containing an exact bottom fact can now produce `False` and close an
+arbitrary target. The next frontend layer selects that refutation schema and
+joins one refuted child with one ordinary target child.
+
+# Next step
+
+Finish focused and static checks, push the exact head for review, then ensure
+the refutation frontend and useful ReLU branch remain based on this repaired
+runtime stack.
+
+# Blockers
+
+None.

progress/20260811T170431Z.md

@@ -0,0 +1,18 @@
+# Accomplished
+
+- Propagated both compile-checked modeled-goal axiom reports through
+  proof-producing contradiction closure.
+
+# Current frontier
+
+Refutation remains tied to exact established facts; inherited goal-proof
+canaries retain explicit standard-axiom checks.
+
+# Next step
+
+Push after focused builds, then continue through mixed refutation frontend and
+useful branch-dependent closure.
+
+# Blockers
+
+None.

progress/20260814T144345Z.md

@@ -0,0 +1,32 @@
+# PR #9221 reconciliation
+
+## Accomplished
+
+- Replayed the approved package-owned refutation feature onto exact current
+  `main`, preserving the merged branch-runtime provenance and state repairs.
+- Audited the newer proof-plan SPEC additions against the single-fact
+  `RefuteSchema`: the current API proves an exact established bottom or
+  inconsistent fact impossible and does not consume runtime contradiction
+  state. The later two-`FactId` endpoint-close sketch still needs a
+  domain-checked meet-to-one-fact lowering; that evidence bridge remains
+  explicitly future work.
+- Added a guarded kernel-axiom report for the ordinary refutation theorem.
+- Added an independent concrete-model witness showing that the rejected `.all`
+  fact is satisfiable, and used the standard transparent replay eliminator.
+- Built the focused proof-emitter, refutation, and exponential conformance
+  targets and ran the repository structural, trust, freshness, and Phase 4
+  checks.
+
+## Current frontier
+
+- The refutation schema, first real `.empty` adapter, exact-fact replay, and
+  positive/negative conformance canaries are reconciled and locally green.
+
+## Next step
+
+- Push the reconciled PR, obtain a fresh exact-head independent review, and
+  monitor exact-head CI to completion.
+
+## Blockers
+
+- None.

scripts/bench/proof_only_runtime_exemptions.json

@@ -137,6 +137,12 @@
     "current_blob": "e0b65d612b56feae1fc9f239addea5d045266526",
     "reason": "Additionally registers the Mathlib-free checked interval branch-start transition only; the factorization service target and executable dependency graph are unchanged."
   },
+  {
+    "path": "lakefile.lean",
+    "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
+    "current_blob": "30eb799f4c1194c115756da0d02d9027735ecb82",
+    "reason": "Additionally registers Mathlib refutation conformance only; the factorization service target and executable dependency graph are unchanged."
+  },
   {
     "path": "HexBerlekamp/FactorTacticTests.lean",
     "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",