Join proved and proof-refuted branch leaves

HexInterval/Experiment/ProofFrontend.lean

@@ -160,6 +160,44 @@ def closeTarget [BEq Fact] (context : Context Fact Handle)
         actualTerm, requestedTerm, established.proof]
   replayResult result
 
+/-- Emit a package-owned refutation of one exact established fact version.
+
+The recognizer table only selects a declaration.  The emitted
+`ProofEmitter.replayRefute` application rechecks that declaration against the
+exact fact and can produce the target only when the fact's proof is already in
+the chronology evidence table. -/
+def refuteFact [BEq Fact] (context : Context Fact Handle)
+    (state : State Fact) (table : RefuteTable Fact Handle)
+    (seen : SeenVersion) (fact : Fact) (target : NodeFact Fact) : MetaM Expr := do
+  let some established := findFact? state.known seen fact
+    | throwError "interval frontend: refuted fact version has not been proved"
+  let some handle := table.find? fact
+    | throwError "interval frontend: no unique refutation schema accepts the fact"
+  let declaration ← context.resolveSchema handle
+  discard <| getConstInfo declaration
+  let exactFact ← context.encoder.nodeFact { node := seen.node, fact }
+  let targetTerm ← context.encoder.nodeFact target
+  let result ←
+    mkAppM ``ProofEmitter.replayRefute
+      #[mkConst declaration, state.program, context.baseFactsTerm,
+        exactFact, targetTerm, established.proof]
+  replayResult result
+
+/-- Select a refutable fact from supplied fact/version snapshot arrays, require
+that exact node, version, and fact in the proof table, and emit arbitrary target
+closure from its semantic impossibility.
+
+The arrays are untrusted selector data; the live caller supplies its retained
+engine arrays. Runtime contradiction state is intentionally not an argument,
+and only the chronology proof found in `state` enters the emitted theorem. -/
+def refuteCurrent [BEq Fact] (context : Context Fact Handle)
+    (state : State Fact) (table : RefuteTable Fact Handle)
+    (facts : Array Fact) (versions : Array Nat) (target : NodeFact Fact) :
+    MetaM Expr := do
+  let some (seen, fact, _) := table.current? facts versions
+    | throwError "interval frontend: no current fact has a unique refutation schema"
+  refuteFact context state table seen fact target
+
 /-- Seed caller-owned version-zero facts by exact positions in the base list. -/
 def seedBase (context : Context Fact Handle) (program : Expr) (basePrefix : Expr) :
     MetaM (List (FactProof Fact)) := do

HexInterval/Experiment/ProofRegistry.lean

@@ -13,39 +13,83 @@ public import HexInterval.Experiment.ProofEmitter
 /-!
 # Joint semantic and proof-emitter package assembly
 
-An executable propagator package, its semantic replay schemas, and its tactic
-emission handles are three views of one extension point.  This module keeps
-the latter two views in one descriptor and checks them against the executable
-registry in the same package order.
+An executable propagator package, its semantic replay schemas, its tactic
+emission handles, and any fact-domain refutation declarations are views of one
+extension point.  This module keeps the proof-facing views in one descriptor
+and checks event schemas against the executable registry in the same package
+order.
 
-The full replay key includes the rule, event role, and payload schema.  Joint
+The full event replay key includes the rule, event role, and payload schema.  Joint
 assembly requires exact package-local equality of those keys: an emitter may
 neither omit a semantic schema nor borrow one from another package.  The
 frontend therefore remains function-agnostic without maintaining a second,
-potentially divergent registry by hand.
+potentially divergent registry by hand. Refutations have no engine event key;
+their exact-fact recognizers are only untrusted selectors for kernel-checked
+`RefuteSchema` applications.
 -/
 
 namespace Hex.Interval.Experiment.ProofRegistry
 
 open Propagator PayloadArena SemanticReplay ProofEmitter
 
+/-- One package-owned recognizer and declaration handle for contradictory
+facts.  Recognition is untrusted planning: the selected declaration must still
+return a `RefuteSchema` accepting the exact fact when the emitted application
+is kernel checked. -/
+structure RefuteRef (Fact Handle : Type) where
+  accepts : Fact → Bool
+  handle : Handle
+
+/-- Refutation recognizers assembled in package order.  More than one match is
+ambiguous and therefore has no selected handle. -/
+structure RefuteTable (Fact Handle : Type) where
+  entries : List (RefuteRef Fact Handle)
+
+namespace RefuteTable
+
+/-- Select the unique package-owned refutation declaration for one exact fact. -/
+def find? (table : RefuteTable Fact Handle) (fact : Fact) : Option Handle :=
+  match table.entries.filter (fun entry => entry.accepts fact) with
+  | [entry] => some entry.handle
+  | _ => none
+
+/-- Select the first current fact with one unambiguous refutation declaration.
+The returned version and fact are the exact values later required from the
+proof table; array mismatch or absence fails closed. -/
+def current? (table : RefuteTable Fact Handle) (facts : Array Fact)
+    (versions : Array Nat) : Option (SeenVersion × Fact × Handle) := do
+  if facts.size != versions.size then none
+  for index in [0:facts.size] do
+    let some fact := facts[index]? | none
+    let some version := versions[index]? | none
+    if let some handle := table.find? fact then
+      return ({ node := { index }, version }, fact, handle)
+  none
+
+end RefuteTable
+
 /-- The proof-facing declarations contributed by one executable package.
 
-`semantic` contains the package-owned checkers and the corresponding `emit`
-fragment contains exactly the handles a tactic may use to apply them. -/
+`semantic` contains the package-owned event checkers, the corresponding `emit`
+fragment contains exactly the handles a tactic may use to apply them, and
+`refute` contributes optional contradiction-leaf declarations. -/
 structure Package (semantics : Semantics Fact) (Handle : Type) where
   semantic : SemanticReplay.Package semantics
   emit : EmitPackage Handle
+  refute : List (RefuteRef Fact Handle) := []
 
 /-- A semantic registry and emitter table assembled from the same packages. -/
 structure Registry (semantics : Semantics Fact) (Handle : Type) where
   private mk ::
   semantic : SemanticReplay.Registry semantics
   emit : SchemaTable Handle
+  refute : RefuteTable Fact Handle
 
-private def make (semantic : SemanticReplay.Registry semantics)
-    (emit : SchemaTable Handle) : Registry semantics Handle :=
-  { semantic, emit }
+private def make {Fact Handle : Type} {semantics : Semantics Fact}
+    (semantic : SemanticReplay.Registry semantics)
+    (emit : SchemaTable Handle) (refute : RefuteTable Fact Handle) :
+    Registry semantics Handle :=
+  { semantic, emit, refute }
 
 /-- Failures specific to joint proof-package assembly.
 
@@ -128,6 +172,9 @@ opaque build (executable : Propagator.Registry Fact)
   | .ok _ =>
       match SchemaTable.build emitPackages with
       | none => throw BuildError.invalidEmit
-      | some emit => pure (make semantic emit)
+      | some emit =>
+          let refute :=
+            { entries := packages.toList.flatMap (fun package => package.refute) }
+          pure (make semantic emit refute)
 
 end Hex.Interval.Experiment.ProofRegistry

HexInterval/SPEC/hex-interval.md

@@ -1654,19 +1654,31 @@ 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.
+
+`ProofRegistry.Package` also contributes optional fact recognizers and
+refutation handles. Lookup accepts exactly one matching handle; no match or an
+ambiguous match fails closed. The low-level frontend treats its supplied fact
+and version arrays as untrusted selector data; the live child passes its exact
+retained engine arrays. For any selected fact, the frontend requires the same
+node, version, and value in its chronology evidence table before it applies the
+schema and produces the child target by ordinary elimination. Arbitrary arrays
+cannot create evidence, but this helper does not itself certify their identity
+with an engine snapshot. Its first mixed join splits the exponential output:
+the left child closes directly from `.nonnegative`, while the right child
+starts from `.negative`, replays the exponential proposal to derive `.empty`,
+and closes only through `replayRefute`. The runtime contradiction result
+selects this path but is not an argument to any emitted proof combinator. 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.
+node. The current frontend consumes an already-installed single contradictory
+fact; the two-proof lowering remains part of the open tree-frontend bridge.
 
 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
@@ -1700,10 +1712,12 @@ These choices may change performance and certificate size, but not the
 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. Remaining acceptance tests include a useful branch-dependent
-two-sided closure, one contradiction leaf plus one target leaf, a nested split,
-a child-local instantiation, a sibling-reference attack, a non-interior
-repeated split, and fuel exhaustion with no theorem emitted.
+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.
 
 ### Proof-producing frontend
 
@@ -1755,16 +1769,26 @@ safety comes from constant lookup, ordinary Lean typechecking, and the replay
 transition's exact key check; only the resulting well-typed theorem
 application enters the kernel.
 `ProofRegistry.Package` now joins each package's semantic schemas and emitter
-fragment. Joint assembly first uses the semantic registry check to establish
-exact package-for-package ownership and bidirectional coverage against the
+fragment, plus any domain-level refutation recognizers owned by that package.
+Joint assembly first uses the semantic registry check to establish exact
+package-for-package ownership and bidirectional coverage against the
 executable formats. It then requires package-local equality of semantic and
-emitter replay-key sets and global emitter uniqueness. Consequently a handle
-cannot be omitted, added under an undeclared key, or borrowed from another
-package even if the final flattened key set would happen to match. The live
-real-sine semantic replay and direct-emission table are both projections of
-this one checked registry. This governance relation is still defense in depth
-rather than part of theorem soundness: every selected schema must produce the
-required kernel-checked claim.
+emitter replay-key sets and global emitter uniqueness. Consequently an event
+handle cannot be omitted, added under an undeclared key, or borrowed from
+another package even if the final flattened key set would happen to match.
+Refutation handles have no executable event key; exact-fact lookup instead
+requires a unique matching recognizer, and the selected `RefuteSchema` must
+accept the same fact during kernel-checked replay. The live real-sine semantic
+replay and direct-emission table are both projections of this one checked
+registry. This governance relation is still defense in depth rather than part
+of theorem soundness: every selected schema must produce the required
+kernel-checked claim.
+
+The current real adapter places its domain-wide `.empty` refuter in the source
+proof package solely to give it one registry-owned lookup position. The theorem
+is about fact-domain bottom semantics, not the source operation. A second
+matching owner would make lookup ambiguous and fail closed; a future explicit
+domain-schema home may replace this provisional ownership convention.
 
 A Mathlib companion must instantiate those abstract schemas, decode each
 frozen entry independently of package cache state, and recheck the

HexIntervalMathlib/Experiment/ExpSign.lean

@@ -173,9 +173,16 @@ def expEmit : EmitPackage Lean.Name :=
       [{ key := expFactSchema.key
          handle := ``expFactSchema }] }
 
+/-- The source package is the designated registry owner for the domain-wide
+bottom refuter. This ownership supplies one unambiguous lookup position; the
+`.empty` theorem itself is fact-domain semantics, not source-operation
+semantics. -/
 def sourceProof : ProofRegistry.Package semantics Lean.Name :=
   { semantic := { factSchemas := #[] }
-    emit := sourceEmit }
+    emit := sourceEmit
+    refute :=
+      [{ accepts := fun fact => fact == .empty
+         handle := ``emptyRefute }] }
 
 def expProof : ProofRegistry.Package semantics Lean.Name :=
   { semantic := { factSchemas := #[expFactSchema] }