feat(interval): prove exact dyadic fact semantics

HexInterval/SPEC/hex-interval.md

@@ -175,6 +175,16 @@ public namespace is itself revisitable before release if qualification proves
 awkward. Unless a block explicitly says otherwise, unqualified API sketches
 below are declarations inside `Hex.Interval`.
 
+The bundled candidate now has a Mathlib companion interpreting every canonical
+fact as a subset of `ℝ`. It proves that a successful executable `intersect`
+denotes logical conjunction for the complete cut language: strict and closed
+ends, tied endpoints, empty results, and either end unbounded. That theorem is
+installed as the generic `FactDomainSchema.proveMeet` boundary, and the
+transparent proof frontend uses it to close a weaker requested interval from a
+stronger established one. This validates the semantic interface without
+settling the representation comparison or adding a function case to the
+frontend.
+
 The comments describe cuts as viewed from outside the interval. In semantic
 notation, a finite lower cut `(a, false)` means `a ≤ x`, and `(a, true)` means
 `a < x`. A finite upper cut `(b, false)` means `x ≤ b`, and `(b, true)` means
@@ -1360,10 +1370,12 @@ one replay schema. The same policy session, joint package registry,
 fact-polymorphic quotation, shared structural encoder, and generic evidence
 fold produce the ordinary theorem `0 ≤ Real.exp x`. Thus both a multi-package
 graph-growing sine proof and a single-rule exponential proof pass through the
-same frontend API without a function switch. The goal reifier below derives
-candidate context pieces from an arbitrary caller expression, but generic
-proof emission has not yet bound its recorded seed recipe to the frontend's
-declared base list.
+same frontend API without a function switch. The reusable proof-emission
+module does not construct the seed-to-input binding by itself. The exponential
+client now sets the runtime and proof-side declared base lists to the same
+reified facts, checks every seeded lookup definitionally, proves the recorded
+hypothesis recipes, and supplies the resulting premise to closure. A reusable
+`InitialContext`-style constructor remains future API work.
 
 The first goal-reification experiment now derives the exponential canary's
 base program, version-zero fact array, and target fact from the actual Lean

conformance/HexIntervalMathlib/DyadicIntervalConformance.lean

@@ -0,0 +1,124 @@
+/-
+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.DyadicInterval
+import HexInterval.Experiment.ProofEmitter
+
+/-!
+# Exact interval semantics conformance
+
+These checks connect the Mathlib-free interval implementation to its real-set
+meaning.  They deliberately mix strict and closed cuts and independently
+unbounded inputs, then use the generic proof-emission closure combinator.
+-/
+
+namespace Hex.IntervalMathlib.DyadicIntervalConformance
+
+open Hex.Interval Hex.Interval.Experiment
+open Propagator SemanticReplay ProofEmitter
+open DyadicInterval
+
+private def real : DomainId := { index := 0 }
+
+private def source : Operation :=
+  { key := { name := "dyadic-semantics.source" }, inputs := [], output := real }
+
+private def sourceNode : Node :=
+  { domain := real, op := { index := 0 }, args := [] }
+
+private def program : Program :=
+  { operations := #[source], nodes := #[sourceNode] }
+
+private def node : NodeId := { index := 0 }
+
+private def limit : EndpointLimit :=
+  { maxEndpointHeight := 64, maxAlignmentShift := 64 }
+
+private def fact (lower : Lower) (upper : Upper)
+    (consistent : (Raw.bounds lower upper).CutConsistent) : Fact :=
+  ⟨.bounds lower upper, consistent⟩
+
+private def closedZeroTwo : Fact :=
+  fact (.finite 0 false) (.finite 2 false) (by decide)
+
+private def openZeroThree : Fact :=
+  fact (.finite 0 true) (.finite 3 false) (by decide)
+
+private def openZeroTwo : Fact :=
+  fact (.finite 0 true) (.finite 2 false) (by decide)
+
+private def nonnegative : Fact :=
+  fact (.finite 0 false) .unbounded (by decide)
+
+private def belowThree : Fact :=
+  fact .unbounded (.finite 3 true) (by decide)
+
+private def zeroThree : Fact :=
+  fact (.finite 0 false) (.finite 3 true) (by decide)
+
+private def singletonZero : Fact :=
+  fact (.finite 0 false) (.finite 0 false) (by decide)
+
+private def positive : Fact :=
+  fact (.finite 0 true) .unbounded (by decide)
+
+private def trivialModels (_ : Program) (_ : NodeId → ℝ) : Prop := True
+
+private def semantics := DyadicInterval.realSemantics trivialModels
+
+private def domain := DyadicInterval.factSchema limit trivialModels
+
+#guard intersect limit closedZeroTwo openZeroThree == .ready openZeroTwo
+#guard intersect limit nonnegative belowThree == .ready zeroThree
+#guard intersect limit singletonZero positive == .ready .empty
+
+/-- Strictness and endpoint selection are reflected exactly in real
+membership, not merely in the executable representation. -/
+example (x : ℝ) :
+    openZeroTwo.Contains x ↔
+      closedZeroTwo.Contains x ∧ openZeroThree.Contains x := by
+  exact contains_intersect (limit := limit) (by decide) x
+
+/-- Independently unbounded inputs intersect to the expected half-open
+bounded interval. -/
+example (x : ℝ) :
+    zeroThree.Contains x ↔ nonnegative.Contains x ∧ belowThree.Contains x := by
+  exact contains_intersect (limit := limit) (by decide) x
+
+/-- A closed singleton and the corresponding strict lower half-line have
+empty intersection. -/
+example (x : ℝ) :
+    Fact.empty.Contains x ↔ singletonZero.Contains x ∧ positive.Contains x := by
+  exact contains_intersect (limit := limit) (by decide) x
+
+private def base : List (NodeFact Fact) :=
+  [{ node, fact := openZeroTwo }]
+
+private def established :
+    Evidence (semantics.Entails program base { node, fact := openZeroTwo }) :=
+  ProofEmitter.assumed (by simp [base])
+
+private def closed :
+    Option (Evidence (semantics.Entails program base { node, fact := nonnegative })) :=
+  ProofEmitter.closeFact domain program base node openZeroTwo nonnegative established
+
+#guard closed.isSome
+
+/-- The generic proof frontend can weaken an established exact interval using
+the independent fact-domain theorem. -/
+theorem intervalWeakens :
+    semantics.Entails program base { node, fact := nonnegative } :=
+  ProofEmitter.proofOfReplay closed (by rfl)
+
+/--
+info: 'Hex.IntervalMathlib.DyadicIntervalConformance.intervalWeakens' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound]
+-/
+#guard_msgs in
+#print axioms intervalWeakens
+
+end Hex.IntervalMathlib.DyadicIntervalConformance

lakefile.lean

@@ -333,6 +333,7 @@ lean_lib HexIntervalExperiment where
 
 lean_lib HexIntervalMathlibExperiment where
   globs := #[`HexIntervalMathlib.Experiment.Center,
+    `HexIntervalMathlib.Experiment.DyadicInterval,
     `HexIntervalMathlib.Experiment.SineSign,
     `HexIntervalMathlib.Experiment.ExpSign,
     `HexIntervalMathlib.Experiment.PntLogTable,
@@ -404,7 +405,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.NestedBranchConformance, `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, `HexInterval.SinTenIntervalConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.ReluConformance, `HexIntervalMathlib.RefuteConformance, `HexIntervalMathlib.PntLogTableConformance, `HexIntervalMathlib.PntNestedLogConformance, `HexIntervalMathlib.PntExpTailConformance, `HexIntervalMathlib.PntTable12Conformance, `HexIntervalMathlib.SinTenConformance, `HexIntervalMathlib.SinTenIntervalConformance, `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.NestedBranchConformance, `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, `HexInterval.SinTenIntervalConformance, `HexIntervalMathlib.DyadicIntervalConformance, `HexIntervalMathlib.SineSignConformance, `HexIntervalMathlib.SineProofConformance, `HexIntervalMathlib.SineTacticConformance, `HexIntervalMathlib.ProofRegistryConformance, `HexIntervalMathlib.ExpSignConformance, `HexIntervalMathlib.ReluConformance, `HexIntervalMathlib.RefuteConformance, `HexIntervalMathlib.PntLogTableConformance, `HexIntervalMathlib.PntNestedLogConformance, `HexIntervalMathlib.PntExpTailConformance, `HexIntervalMathlib.PntTable12Conformance, `HexIntervalMathlib.SinTenConformance, `HexIntervalMathlib.SinTenIntervalConformance, `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/20260811T181434Z.md

@@ -0,0 +1,28 @@
+# Accomplished
+
+- Added real-set semantics for the checked dyadic interval fact domain,
+  including strict, closed, empty, and independently unbounded cuts.
+- Proved that every successful executable intersection denotes exactly the
+  conjunction of its input facts.
+- Installed that theorem behind the function-independent fact-domain schema.
+- Added kernel-checked conformance for strict ties, unbounded intersections,
+  empty intersections, and generic frontend weakening through `closeFact`.
+- Clarified that the reusable emitter does not itself construct the
+  seed-to-input binding, while the exponential client supplies that binding.
+
+# Current frontier
+
+The generic proof frontend now has an exact real semantic interpretation for
+the concrete interval facts used by arbitrary propagators. The semantic bridge
+does not yet provide proof schemas for the existing arithmetic and centered
+function packages.
+
+# Next step
+
+Give the existing centered arbitrary-function contractor a package-owned real
+soundness schema over this fact domain, then run it through the same live
+policy and proof frontend without adding a function case to generic code.
+
+# Blockers
+
+None.

progress/20260814T203222Z.md

@@ -0,0 +1,37 @@
+# PR #9227 local reconciliation
+
+## Accomplished
+
+- Replayed only the exact dyadic fact-semantics feature onto exact merged
+  #9226 main `591a3315bc6a61cdb118d399640fa4a3d933c62a`.
+- Preserved the nested-branch and complete PNT log-table, nested-log, and
+  exponential-tail registrations while adding the Mathlib semantic companion
+  and its conformance target.
+- Audited the open, closed, empty, tied-endpoint, and independently unbounded
+  membership semantics; the checked-comparison bridge; normalization of only
+  semantically empty inconsistent cuts; and the universal exact-intersection
+  theorem.
+- Verified that `factSchema.proveMeet` recomputes intersection proof-side,
+  returns evidence only for the exact installed fact, and keeps operation
+  models and runtime narrowing data outside the evidence boundary.
+- Confirmed the generic weakening canary is nonvacuous and its ordinary theorem
+  has the guarded expected axiom report.
+- Recomputed the proof-only Lake exemption for exact resolved blob
+  `79d5dad91a2cf3ab7b4bb359856a00bf79f3619e`.
+- Built the focused dyadic-semantics and inherited interval targets and passed
+  the static, trust-surface, freshness, PNT-inventory, diff, and banned-term
+  checks.
+
+## Current frontier
+
+- The feature is prepared as a clean local commit on merged #9226 and remains
+  intentionally unpushed while the Table12 probe may advance `main`.
+
+## Next step
+
+- Rebase once onto the final post-Table12 `main` if it moves, refresh only exact
+  freshness metadata, then run final independent review and exact-head CI.
+
+## Blockers
+
+- None.

progress/20260814T211642Z.md

@@ -0,0 +1,30 @@
+# PR #9227 final reconciliation
+
+## Accomplished
+
+- Rebased the audited exact dyadic fact-semantics feature onto exact post-Table12
+  main `c216fe2fb744cac7d503511c68402a03c9aeaea2`.
+- Preserved the complete PNT log-table, nested-log, exponential-tail, and
+  Table12 experiments and conformance registrations, together with the nested
+  branch and earlier interval content.
+- Refreshed the narrow proof-only Lake exemption to exact resolved blob
+  `db3b912684e66f7e9759d5e19e9695b262211fc0`.
+- Rebuilt the dyadic semantics, nested branch, ReLU, and all PNT targets and
+  reran the static, trust-surface, freshness, inventory, diff, and banned-term
+  checks successfully.
+- Kept the prepared #9228 centered-function commits isolated on their local
+  lineage; they are not part of this candidate.
+
+## Current frontier
+
+- The exact #9227 candidate is ready to push for final independent review and
+  exact-head CI.
+
+## Next step
+
+- Push and retarget PR #9227 to `main`, then require fresh Opus approval and
+  exact-head CI success before marking it merge-ready.
+
+## Blockers
+
+- None.

scripts/bench/proof_only_runtime_exemptions.json

@@ -191,6 +191,12 @@
     "current_blob": "a869c195af5b211b96e848d4f11754abb64ebcc8",
     "reason": "Additionally registers the Mathlib-free HexInterval nested-branch conformance module only; the factorization service target and executable dependency graph are unchanged."
   },
+  {
+    "path": "lakefile.lean",
+    "baseline_blob": "6dd80771ae2212333b2a9b925b52056e0037ff56",
+    "current_blob": "db3b912684e66f7e9759d5e19e9695b262211fc0",
+    "reason": "Additionally registers the proof-only real-semantics companion for exact interval facts and its conformance module; the factorization service target and executable dependency graph are unchanged."
+  },
   {
     "path": "HexBerlekamp/FactorTacticTests.lean",
     "baseline_blob": "4063e15934a89c671ac72d201fa60c2ef6feaf59",