From c7f2001d4e782f1273cbccc5d4e134db7af2032c Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Mon, 27 Jul 2026 10:59:41 +0000
Subject: [PATCH 1/3] feat(interval): replay rational arithmetic edges

---
 HexInterval/Experiment/RationalEdge.lean      | 829 ++++++++++++++++++
 .../HexInterval/RationalEdgeConformance.lean  | 233 +++++
 lakefile.lean                                 |   6 +-
 progress/20260727T105900Z.md                  |  50 ++
 4 files changed, 1116 insertions(+), 2 deletions(-)
 create mode 100644 HexInterval/Experiment/RationalEdge.lean
 create mode 100644 conformance/HexInterval/RationalEdgeConformance.lean
 create mode 100644 progress/20260727T105900Z.md

diff --git a/HexInterval/Experiment/RationalEdge.lean b/HexInterval/Experiment/RationalEdge.lean
new file mode 100644
index 000000000..cb4778464
--- /dev/null
+++ b/HexInterval/Experiment/RationalEdge.lean
@@ -0,0 +1,829 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import HexInterval.Experiment.RationalTable
+
+@[expose] public section
+
+/-!
+# Resource-preflighted rational arithmetic edges
+
+This module adds a first Mathlib-free arithmetic replay boundary for canonical
+raw rational tables.  Its edge language is deliberately independent of an
+interval propagation strategy: edges merely assert exact arithmetic or order
+relations between table slots.
+
+The checker has three strictly ordered phases:
+
+1. validate the complete rational table and bound the edge collection;
+2. validate every index and all caller-owned lookup, temporary-width, and
+   arithmetic-work limits while constructing a bounded resolved `List`;
+3. replay naive integer identities and report the first false edge.
+
+Thus no checked cross-product is formed unless the entire edge list passes
+preflight.  Indexed `List` lookup is charged by the exact number of constructors
+visited (`index + 1` for every valid reference).  Temporary widths use the
+standard conservative bounds `bits (x*y) <= bits x + bits y` and the analogous
+sum-or-difference bound `max (bits x) (bits y) + 1`.  Arithmetic work is an
+explicit schoolbook proxy: multiplying widths costs their product, and either
+adding or comparing two temporaries costs the larger width.  These formulas inspect only the bit
+lengths of already-retained inputs; they do not allocate any arithmetic
+cross-product.
+
+This is an experiment, not a frozen storage or certificate format.  In
+particular it adds no interval projection, wire decoder, cancellation-aware
+replay, planner policy, or tactic frontend.
+-/
+
+namespace Hex.Interval.Experiment.RationalEdge
+
+open Center RationalTable
+
+/-! ## Strategy-neutral edge language -/
+
+/-- An exact arithmetic or comparison assertion over rational-table indices. -/
+inductive ArithEdge where
+  | add (left right result : Nat)
+  | sub (left right result : Nat)
+  | mul (left right result : Nat)
+  | inv (input result : Nat)
+  | eq (left right : Nat)
+  | le (left right : Nat)
+  | lt (left right : Nat)
+  deriving DecidableEq, Repr
+
+/-- Stable names for references in deterministic index failures. -/
+inductive Reference where
+  | left
+  | right
+  | input
+  | result
+  deriving DecidableEq, Repr
+
+/-- Caller-owned limits for the arithmetic-edge boundary. -/
+structure Limit where
+  maxEdges : Nat
+  maxLookupSteps : Nat
+  maxTemporaryBits : Nat
+  maxArithmeticWork : Nat
+  deriving DecidableEq, Repr
+
+/-- Logical failures found without accepting a false identity. -/
+inductive Invalid where
+  | badIndex (reference : Reference) (index : Nat)
+  | resolutionMismatch
+  | wrongIdentity
+  deriving DecidableEq, Repr
+
+/-- Edge-specific resource failures.  Raw-table failures retain the separate
+`RawRat.Resource` vocabulary. -/
+inductive Resource where
+  | edges
+  | lookupSteps
+  | temporaryBits
+  | arithmeticWork
+  deriving DecidableEq, Repr
+
+/-- Deterministic public result.  Collection failures have no edge index;
+per-edge failures identify the first failing edge. -/
+inductive Result where
+  | ready
+  | malformedTable (index : Nat) (reason : RawRat.Invalid)
+  | tableResource (index : Option Nat) (reason : RawRat.Resource)
+  | malformedEdge (index : Nat) (reason : Invalid)
+  | edgeResource (index : Option Nat) (reason : Resource)
+  deriving DecidableEq, Repr
+
+namespace ArithEdge
+
+/-- Exact `List` traversal cost of all references in one valid edge. -/
+def lookupSteps : ArithEdge → Nat
+  | .add left right result | .sub left right result | .mul left right result =>
+      (left + 1) + (right + 1) + (result + 1)
+  | .inv input result => (input + 1) + (result + 1)
+  | .eq left right | .le left right | .lt left right =>
+      (left + 1) + (right + 1)
+
+/-- Return the first out-of-range reference in constructor field order.  This
+uses only comparisons with the already-bounded table length. -/
+def firstBadIndex (tableSize : Nat) : ArithEdge → Option (Reference × Nat)
+  | .add left right result | .sub left right result | .mul left right result =>
+      if tableSize ≤ left then some (.left, left)
+      else if tableSize ≤ right then some (.right, right)
+      else if tableSize ≤ result then some (.result, result)
+      else none
+  | .inv input result =>
+      if tableSize ≤ input then some (.input, input)
+      else if tableSize ≤ result then some (.result, result)
+      else none
+  | .eq left right | .le left right | .lt left right =>
+      if tableSize ≤ left then some (.left, left)
+      else if tableSize ≤ right then some (.right, right)
+      else none
+
+end ArithEdge
+
+/-! ## Resolved arithmetic and allocation-independent costs -/
+
+/-- A preflighted edge with table entries resolved.  Values are shared from
+the input list; no rational arithmetic result is retained here. -/
+inductive Resolved where
+  | add (left right result : RawRat)
+  | sub (left right result : RawRat)
+  | mul (left right result : RawRat)
+  | inv (input result : RawRat)
+  | eq (left right : RawRat)
+  | le (left right : RawRat)
+  | lt (left right : RawRat)
+  deriving DecidableEq, Repr
+
+/-- Preflight cost of one resolved edge.  `temporaryBits` is a maximum while
+`arithmeticWork` is additive across all primitive operations in the identity. -/
+structure Cost where
+  temporaryBits : Nat
+  arithmeticWork : Nat
+  deriving DecidableEq, Repr
+
+namespace Cost
+
+/-- Conservative width of a product from operand widths. -/
+def mulBits (left right : Nat) : Nat :=
+  if left = 0 || right = 0 then 0 else left + right
+
+/-- Conservative width of a signed sum or difference. -/
+def addBits (left right : Nat) : Nat :=
+  if left = 0 then right
+  else if right = 0 then left
+  else max left right + 1
+
+/-- Schoolbook multiplication work proxy. -/
+def mulWork (left right : Nat) : Nat := left * right
+
+end Cost
+
+namespace Resolved
+
+/-- Allocation-independent preflight cost for one naive identity. -/
+def cost : Resolved → Cost
+  | .add left right result | .sub left right result =>
+      let lc := left.cost
+      let rc := right.cost
+      let oc := result.cost
+      let denominatorBits := Cost.mulBits lc.denominatorBits rc.denominatorBits
+      let leftTermBits := Cost.mulBits lc.numeratorBits rc.denominatorBits
+      let rightTermBits := Cost.mulBits rc.numeratorBits lc.denominatorBits
+      let numeratorBits := Cost.addBits leftTermBits rightTermBits
+      let leftResultBits := Cost.mulBits oc.numeratorBits denominatorBits
+      let rightResultBits := Cost.mulBits numeratorBits oc.denominatorBits
+      { temporaryBits := max denominatorBits <| max leftTermBits <|
+          max rightTermBits <| max numeratorBits <|
+          max leftResultBits rightResultBits
+        arithmeticWork :=
+          Cost.mulWork lc.denominatorBits rc.denominatorBits +
+          Cost.mulWork lc.numeratorBits rc.denominatorBits +
+          Cost.mulWork rc.numeratorBits lc.denominatorBits +
+          (max leftTermBits rightTermBits + 1) +
+          Cost.mulWork oc.numeratorBits denominatorBits +
+          Cost.mulWork numeratorBits oc.denominatorBits +
+          max leftResultBits rightResultBits }
+  | .mul left right result =>
+      let lc := left.cost
+      let rc := right.cost
+      let oc := result.cost
+      let numeratorBits := Cost.mulBits lc.numeratorBits rc.numeratorBits
+      let denominatorBits := Cost.mulBits lc.denominatorBits rc.denominatorBits
+      let leftResultBits := Cost.mulBits oc.numeratorBits denominatorBits
+      let rightResultBits := Cost.mulBits numeratorBits oc.denominatorBits
+      { temporaryBits := max numeratorBits <| max denominatorBits <|
+          max leftResultBits rightResultBits
+        arithmeticWork :=
+          Cost.mulWork lc.numeratorBits rc.numeratorBits +
+          Cost.mulWork lc.denominatorBits rc.denominatorBits +
+          Cost.mulWork oc.numeratorBits denominatorBits +
+          Cost.mulWork numeratorBits oc.denominatorBits +
+          max leftResultBits rightResultBits }
+  | .inv input result =>
+      let ic := input.cost
+      let rc := result.cost
+      if ic.numeratorBits = 0 then
+        { temporaryBits := 0
+          arithmeticWork := rc.numeratorBits }
+      else
+        let leftResultBits := Cost.mulBits rc.numeratorBits ic.numeratorBits
+        let rightResultBits := Cost.mulBits ic.denominatorBits rc.denominatorBits
+        { temporaryBits := max leftResultBits rightResultBits
+          arithmeticWork :=
+            ic.numeratorBits +
+            Cost.mulWork rc.numeratorBits ic.numeratorBits +
+            Cost.mulWork ic.denominatorBits rc.denominatorBits +
+            max leftResultBits rightResultBits }
+  | .eq left right | .le left right | .lt left right =>
+      let lc := left.cost
+      let rc := right.cost
+      let leftResultBits := Cost.mulBits lc.numeratorBits rc.denominatorBits
+      let rightResultBits := Cost.mulBits rc.numeratorBits lc.denominatorBits
+      { temporaryBits := max
+          leftResultBits rightResultBits
+        arithmeticWork :=
+          Cost.mulWork lc.numeratorBits rc.denominatorBits +
+          Cost.mulWork rc.numeratorBits lc.denominatorBits +
+          max leftResultBits rightResultBits }
+
+/-- Naive addition identity, without normalization or cancellation. -/
+def checkAdd (left right result : RawRat) : Bool :=
+  let commonDenominator := left.den * right.den
+  let numerator := left.num * (right.den : Int) + right.num * (left.den : Int)
+  result.num * (commonDenominator : Int) == numerator * (result.den : Int)
+
+/-- Naive subtraction identity, without normalization or cancellation. -/
+def checkSub (left right result : RawRat) : Bool :=
+  let commonDenominator := left.den * right.den
+  let numerator := left.num * (right.den : Int) - right.num * (left.den : Int)
+  result.num * (commonDenominator : Int) == numerator * (result.den : Int)
+
+/-- Naive multiplication identity, without cross-cancellation. -/
+def checkMul (left right result : RawRat) : Bool :=
+  let numerator := left.num * right.num
+  let denominator := left.den * right.den
+  result.num * (denominator : Int) == numerator * (result.den : Int)
+
+/-- Naive inverse identity.  Core rational inversion is total, so zero maps to
+canonical zero; nonzero inputs use the signed cross-product identity. -/
+def checkInv (input result : RawRat) : Bool :=
+  if input.num = 0 then result.num == 0
+  else result.num * input.num == (input.den : Int) * (result.den : Int)
+
+/-- Naive rational equality by positive-denominator cross-products. -/
+def checkEq (left right : RawRat) : Bool :=
+  left.num * (right.den : Int) == right.num * (left.den : Int)
+
+/-- Naive non-strict order by positive-denominator cross-products. -/
+def checkLe (left right : RawRat) : Bool :=
+  left.num * (right.den : Int) ≤ right.num * (left.den : Int)
+
+/-- Naive strict order by positive-denominator cross-products. -/
+def checkLt (left right : RawRat) : Bool :=
+  left.num * (right.den : Int) < right.num * (left.den : Int)
+
+/-- Replay one fully preflighted edge. -/
+def check : Resolved → Bool
+  | .add left right result => checkAdd left right result
+  | .sub left right result => checkSub left right result
+  | .mul left right result => checkMul left right result
+  | .inv input result => checkInv input result
+  | .eq left right => checkEq left right
+  | .le left right => checkLe left right
+  | .lt left right => checkLt left right
+
+/-- Mathematical proposition asserted by a resolved edge. -/
+def Holds : Resolved → Prop
+  | .add left right result => result.value = left.value + right.value
+  | .sub left right result => result.value = left.value - right.value
+  | .mul left right result => result.value = left.value * right.value
+  | .inv input result => result.value = input.value⁻¹
+  | .eq left right => left.value = right.value
+  | .le left right => left.value ≤ right.value
+  | .lt left right => left.value < right.value
+
+/-- Canonicality assumptions supplied by successful complete-table validation. -/
+def Canonical : Resolved → Prop
+  | .add left right result | .sub left right result | .mul left right result =>
+      left.Canonical ∧ right.Canonical ∧ result.Canonical
+  | .inv input result => input.Canonical ∧ result.Canonical
+  | .eq left right | .le left right | .lt left right =>
+      left.Canonical ∧ right.Canonical
+
+end Resolved
+
+/-! ## Core `Rat` soundness -/
+
+namespace RawRat
+
+/-- Canonical raw fields are exactly the fields of their Core `Rat` value. -/
+theorem fields_of_canonical {q : RawRat} (h : q.Canonical) :
+    q.value.num = q.num ∧ q.value.den = q.den := by
+  have hvalue : q.value = Rat.mk' q.num q.den h.1 h.2 := by
+    exact (Rat.mk_eq_mkRat q.num q.den h.1 h.2).symm
+  rw [hvalue]
+  exact ⟨rfl, rfl⟩
+
+end RawRat
+
+namespace Resolved
+
+/-- Soundness of the naive addition cross-product. -/
+theorem add_sound {left right result : RawRat}
+    (hl : left.Canonical) (hr : right.Canonical) (ho : result.Canonical)
+    (h : checkAdd left right result = true) :
+    result.value = left.value + right.value := by
+  have hlf := RawRat.fields_of_canonical hl
+  have hrf := RawRat.fields_of_canonical hr
+  have hid :
+      result.num * ((left.den * right.den : Nat) : Int) =
+        (left.num * (right.den : Int) + right.num * (left.den : Int)) *
+          (result.den : Int) := by
+    simpa [checkAdd] using h
+  rw [Rat.add_def', hlf.1, hlf.2, hrf.1, hrf.2]
+  unfold RawRat.value
+  exact (Rat.mkRat_eq_iff ho.1 (Nat.mul_ne_zero hl.1 hr.1)).2 hid
+
+/-- Soundness of the naive subtraction cross-product. -/
+theorem sub_sound {left right result : RawRat}
+    (hl : left.Canonical) (hr : right.Canonical) (ho : result.Canonical)
+    (h : checkSub left right result = true) :
+    result.value = left.value - right.value := by
+  have hlf := RawRat.fields_of_canonical hl
+  have hrf := RawRat.fields_of_canonical hr
+  have hid :
+      result.num * ((left.den * right.den : Nat) : Int) =
+        (left.num * (right.den : Int) - right.num * (left.den : Int)) *
+          (result.den : Int) := by
+    simpa [checkSub] using h
+  rw [Rat.sub_def', hlf.1, hlf.2, hrf.1, hrf.2]
+  unfold RawRat.value
+  exact (Rat.mkRat_eq_iff ho.1 (Nat.mul_ne_zero hl.1 hr.1)).2 hid
+
+/-- Soundness of the naive multiplication cross-product. -/
+theorem mul_sound {left right result : RawRat}
+    (hl : left.Canonical) (hr : right.Canonical) (ho : result.Canonical)
+    (h : checkMul left right result = true) :
+    result.value = left.value * right.value := by
+  have hlf := RawRat.fields_of_canonical hl
+  have hrf := RawRat.fields_of_canonical hr
+  have hid :
+      result.num * ((left.den * right.den : Nat) : Int) =
+        (left.num * right.num) * (result.den : Int) := by
+    simpa [checkMul] using h
+  rw [Rat.mul_def', hlf.1, hlf.2, hrf.1, hrf.2]
+  unfold RawRat.value
+  exact (Rat.mkRat_eq_iff ho.1 (Nat.mul_ne_zero hl.1 hr.1)).2 hid
+
+/-- Soundness of the naive inverse check, including Core's `0⁻¹ = 0`. -/
+theorem inv_sound {input result : RawRat}
+    (hi : input.Canonical) (hr : result.Canonical)
+    (h : checkInv input result = true) :
+    result.value = input.value⁻¹ := by
+  by_cases hn : input.num = 0
+  · have hrn : result.num = 0 := by
+      simpa [checkInv, hn] using h
+    have hi0 : input.value = 0 := by
+      unfold RawRat.value
+      exact (Rat.mkRat_eq_zero hi.1).2 hn
+    have hr0 : result.value = 0 := by
+      unfold RawRat.value
+      exact (Rat.mkRat_eq_zero hr.1).2 hrn
+    rw [hi0, hr0, Rat.inv_zero]
+  · have hif := RawRat.fields_of_canonical hi
+    have hid : result.num * input.num =
+        (input.den : Int) * (result.den : Int) := by
+      simpa [checkInv, hn] using h
+    have hrd : (result.den : Int) ≠ 0 := by
+      exact mt Int.natCast_eq_zero.mp hr.1
+    calc
+      result.value = Rat.divInt result.num (result.den : Int) := by
+        exact (Rat.divInt_ofNat result.num result.den).symm
+      _ = Rat.divInt (input.den : Int) input.num :=
+        (Rat.divInt_eq_divInt_iff hrd hn).2 hid
+      _ = input.value⁻¹ := by
+        rw [Rat.inv_def, hif.1, hif.2]
+
+/-- Soundness of the naive equality cross-product. -/
+theorem eq_sound {left right : RawRat}
+    (hl : left.Canonical) (hr : right.Canonical)
+    (h : checkEq left right = true) : left.value = right.value := by
+  have hlf := RawRat.fields_of_canonical hl
+  have hrf := RawRat.fields_of_canonical hr
+  apply Rat.eq_iff_mul_eq_mul.2
+  rw [hlf.1, hlf.2, hrf.1, hrf.2]
+  simpa [checkEq] using h
+
+/-- Soundness of the naive non-strict order cross-product. -/
+theorem le_sound {left right : RawRat}
+    (hl : left.Canonical) (hr : right.Canonical)
+    (h : checkLe left right = true) : left.value ≤ right.value := by
+  have hlf := RawRat.fields_of_canonical hl
+  have hrf := RawRat.fields_of_canonical hr
+  apply (Rat.le_iff left.value right.value).2
+  rw [hlf.1, hlf.2, hrf.1, hrf.2]
+  simpa [checkLe] using h
+
+/-- Soundness of the naive strict order cross-product. -/
+theorem lt_sound {left right : RawRat}
+    (hl : left.Canonical) (hr : right.Canonical)
+    (h : checkLt left right = true) : left.value < right.value := by
+  have hlf := RawRat.fields_of_canonical hl
+  have hrf := RawRat.fields_of_canonical hr
+  apply (Rat.lt_iff left.value right.value).2
+  rw [hlf.1, hlf.2, hrf.1, hrf.2]
+  simpa [checkLt] using h
+
+/-- Every checked resolved edge is sound in Core `Rat`. -/
+theorem sound {edge : Resolved} (hc : edge.Canonical)
+    (h : edge.check = true) : edge.Holds := by
+  cases edge with
+  | add left right result => exact add_sound hc.1 hc.2.1 hc.2.2 h
+  | sub left right result => exact sub_sound hc.1 hc.2.1 hc.2.2 h
+  | mul left right result => exact mul_sound hc.1 hc.2.1 hc.2.2 h
+  | inv input result => exact inv_sound hc.1 hc.2 h
+  | eq left right => exact eq_sound hc.1 hc.2 h
+  | le left right => exact le_sound hc.1 hc.2 h
+  | lt left right => exact lt_sound hc.1 hc.2 h
+
+end Resolved
+
+/-! ## Full preflight and replay -/
+
+/-- Remaining additive budgets during a preflight scan. -/
+structure Remaining where
+  lookupSteps : Nat
+  arithmeticWork : Nat
+  deriving DecidableEq, Repr
+
+/-- Internal preflight failures exclude `ready` by construction. -/
+inductive PreflightFailure where
+  | malformed (index : Nat) (reason : Invalid)
+  | resource (index : Option Nat) (reason : Resource)
+  deriving DecidableEq, Repr
+
+namespace PreflightFailure
+
+/-- Embed an internal edge-preflight failure into the public result. -/
+def result : PreflightFailure → Result
+  | .malformed index reason => .malformedEdge index reason
+  | .resource index reason => .edgeResource index reason
+
+end PreflightFailure
+
+/-- Internal result of resolving the complete edge list. -/
+inductive Preflight where
+  | ready (plan : List Resolved)
+  | failed (failure : PreflightFailure)
+  deriving DecidableEq, Repr
+
+/-- Resolve an edge after its indices have been checked.  The `none` branch is
+retained rather than replaced by defaults, so any future change to index
+validation still fails closed. -/
+def resolve? (table : List RawRat) : ArithEdge → Option Resolved
+  | .add left right result =>
+      match table[left]?, table[right]?, table[result]? with
+      | some l, some r, some o => some (.add l r o)
+      | _, _, _ => none
+  | .sub left right result =>
+      match table[left]?, table[right]?, table[result]? with
+      | some l, some r, some o => some (.sub l r o)
+      | _, _, _ => none
+  | .mul left right result =>
+      match table[left]?, table[right]?, table[result]? with
+      | some l, some r, some o => some (.mul l r o)
+      | _, _, _ => none
+  | .inv input result =>
+      match table[input]?, table[result]? with
+      | some i, some o => some (.inv i o)
+      | _, _ => none
+  | .eq left right =>
+      match table[left]?, table[right]? with
+      | some l, some r => some (.eq l r)
+      | _, _ => none
+  | .le left right =>
+      match table[left]?, table[right]? with
+      | some l, some r => some (.le l r)
+      | _, _ => none
+  | .lt left right =>
+      match table[left]?, table[right]? with
+      | some l, some r => some (.lt l r)
+      | _, _ => none
+
+namespace ArithEdge
+
+/-- Mathematical meaning of an indexed edge.  Missing indices make the
+proposition false; successful checker use supplies a particular resolved edge. -/
+def Holds (table : List RawRat) (edge : ArithEdge) : Prop :=
+  ∃ resolved, resolve? table edge = some resolved ∧ resolved.Holds
+
+end ArithEdge
+
+/-- A successful optional list lookup returns a member of that list. -/
+theorem mem_of_lookup {table : List RawRat} {index : Nat} {entry : RawRat}
+    (h : table[index]? = some entry) : entry ∈ table := by
+  induction table generalizing index with
+  | nil => simp at h
+  | cons head tail ih =>
+      cases index with
+      | zero =>
+          simp at h
+          subst entry
+          simp
+      | succ index =>
+          simp at h
+          exact List.mem_cons_of_mem head (ih h)
+
+/-- Resolving from a completely validated table preserves canonicality. -/
+theorem canonical_of_resolve {table : List RawRat} {edge : ArithEdge}
+    {resolved : Resolved} (hc : ∀ entry ∈ table, entry.Canonical)
+    (h : resolve? table edge = some resolved) : resolved.Canonical := by
+  cases edge with
+  | add left right result =>
+      cases hl : table[left]? with
+      | none => simp [resolve?, hl] at h
+      | some l =>
+          cases hr : table[right]? with
+          | none => simp [resolve?, hl, hr] at h
+          | some r =>
+              cases ho : table[result]? with
+              | none => simp [resolve?, hl, hr, ho] at h
+              | some o =>
+                  simp [resolve?, hl, hr, ho] at h
+                  subst resolved
+                  exact ⟨hc l (mem_of_lookup hl), hc r (mem_of_lookup hr),
+                    hc o (mem_of_lookup ho)⟩
+  | sub left right result =>
+      cases hl : table[left]? with
+      | none => simp [resolve?, hl] at h
+      | some l =>
+          cases hr : table[right]? with
+          | none => simp [resolve?, hl, hr] at h
+          | some r =>
+              cases ho : table[result]? with
+              | none => simp [resolve?, hl, hr, ho] at h
+              | some o =>
+                  simp [resolve?, hl, hr, ho] at h
+                  subst resolved
+                  exact ⟨hc l (mem_of_lookup hl), hc r (mem_of_lookup hr),
+                    hc o (mem_of_lookup ho)⟩
+  | mul left right result =>
+      cases hl : table[left]? with
+      | none => simp [resolve?, hl] at h
+      | some l =>
+          cases hr : table[right]? with
+          | none => simp [resolve?, hl, hr] at h
+          | some r =>
+              cases ho : table[result]? with
+              | none => simp [resolve?, hl, hr, ho] at h
+              | some o =>
+                  simp [resolve?, hl, hr, ho] at h
+                  subst resolved
+                  exact ⟨hc l (mem_of_lookup hl), hc r (mem_of_lookup hr),
+                    hc o (mem_of_lookup ho)⟩
+  | inv input result =>
+      cases hi : table[input]? with
+      | none => simp [resolve?, hi] at h
+      | some i =>
+          cases ho : table[result]? with
+          | none => simp [resolve?, hi, ho] at h
+          | some o =>
+              simp [resolve?, hi, ho] at h
+              subst resolved
+              exact ⟨hc i (mem_of_lookup hi), hc o (mem_of_lookup ho)⟩
+  | eq left right =>
+      cases hl : table[left]? with
+      | none => simp [resolve?, hl] at h
+      | some l =>
+          cases hr : table[right]? with
+          | none => simp [resolve?, hl, hr] at h
+          | some r =>
+              simp [resolve?, hl, hr] at h
+              subst resolved
+              exact ⟨hc l (mem_of_lookup hl), hc r (mem_of_lookup hr)⟩
+  | le left right =>
+      cases hl : table[left]? with
+      | none => simp [resolve?, hl] at h
+      | some l =>
+          cases hr : table[right]? with
+          | none => simp [resolve?, hl, hr] at h
+          | some r =>
+              simp [resolve?, hl, hr] at h
+              subst resolved
+              exact ⟨hc l (mem_of_lookup hl), hc r (mem_of_lookup hr)⟩
+  | lt left right =>
+      cases hl : table[left]? with
+      | none => simp [resolve?, hl] at h
+      | some l =>
+          cases hr : table[right]? with
+          | none => simp [resolve?, hl, hr] at h
+          | some r =>
+              simp [resolve?, hl, hr] at h
+              subst resolved
+              exact ⟨hc l (mem_of_lookup hl), hc r (mem_of_lookup hr)⟩
+
+/-- Pointwise correspondence between indexed edges and a resolved plan. -/
+inductive Relates (table : List RawRat) : List ArithEdge → List Resolved → Prop where
+  | nil : Relates table [] []
+  | cons {edge edges resolved plan}
+      (head : resolve? table edge = some resolved)
+      (tail : Relates table edges plan) :
+      Relates table (edge :: edges) (resolved :: plan)
+
+/-- Validate and resolve every edge before any identity replay.  Per edge the
+order is index validity, lookup budget, temporary width, aggregate arithmetic
+work, then continuation to the next edge. -/
+def preflightFrom (limit : Limit) (table : List RawRat) (tableSize : Nat) :
+    Nat → Remaining → List ArithEdge → Preflight
+  | _, _, [] => .ready []
+  | edgeIndex, remaining, edge :: tail =>
+      match edge.firstBadIndex tableSize with
+      | some (reference, index) =>
+          .failed (.malformed edgeIndex (.badIndex reference index))
+      | none =>
+          let lookupCost := edge.lookupSteps
+          if lookupCost > remaining.lookupSteps then
+            .failed (.resource (some edgeIndex) .lookupSteps)
+          else
+            match resolve? table edge with
+            | none =>
+                -- Unreachable for the current `firstBadIndex`; kept fail-closed.
+                .failed (.malformed edgeIndex .resolutionMismatch)
+            | some resolved =>
+                let edgeCost := resolved.cost
+                if edgeCost.temporaryBits > limit.maxTemporaryBits then
+                  .failed (.resource (some edgeIndex) .temporaryBits)
+                else if edgeCost.arithmeticWork > remaining.arithmeticWork then
+                  .failed (.resource (some edgeIndex) .arithmeticWork)
+                else
+                  let nextRemaining : Remaining :=
+                    { lookupSteps := remaining.lookupSteps - lookupCost
+                      arithmeticWork :=
+                        remaining.arithmeticWork - edgeCost.arithmeticWork }
+                  match preflightFrom limit table tableSize (edgeIndex + 1)
+                      nextRemaining tail with
+                  | .ready plan => .ready (resolved :: plan)
+                  | .failed failure => .failed failure
+
+/-- Successful full preflight preserves pointwise edge/plan correspondence. -/
+theorem relates_of_preflight {limit : Limit} {table : List RawRat}
+    {tableSize edgeIndex : Nat} {remaining : Remaining}
+    {edges : List ArithEdge} {plan : List Resolved}
+    (h : preflightFrom limit table tableSize edgeIndex remaining edges =
+      .ready plan) : Relates table edges plan := by
+  induction edges generalizing edgeIndex remaining plan with
+  | nil =>
+      simp [preflightFrom] at h
+      subst plan
+      exact .nil
+  | cons edge tail ih =>
+      unfold preflightFrom at h
+      cases hbad : edge.firstBadIndex tableSize with
+      | some bad => simp [hbad] at h
+      | none =>
+          simp only [hbad] at h
+          split at h
+          next => contradiction
+          next =>
+            cases hresolve : resolve? table edge with
+            | none => simp [hresolve] at h
+            | some resolved =>
+                simp only [hresolve] at h
+                split at h
+                next => contradiction
+                next =>
+                  split at h
+                  next => contradiction
+                  next =>
+                    cases htail : preflightFrom limit table tableSize
+                        (edgeIndex + 1)
+                        { lookupSteps := remaining.lookupSteps - edge.lookupSteps
+                          arithmeticWork :=
+                            remaining.arithmeticWork - resolved.cost.arithmeticWork }
+                        tail with
+                    | failed result => simp [htail] at h
+                    | ready tailPlan =>
+                        simp [htail] at h
+                        subst plan
+                        exact .cons hresolve (ih htail)
+
+/-- Replay a completely preflighted plan and return the first false identity. -/
+def replayFrom : Nat → List Resolved → Result
+  | _, [] => .ready
+  | index, edge :: tail =>
+      if edge.check then replayFrom (index + 1) tail
+      else .malformedEdge index .wrongIdentity
+
+/-- Validate a table and its complete arithmetic-edge list.  No cross-product
+in `Resolved.check` is reached until `preflightFrom` has accepted every edge. -/
+def check (tableLimit : RawRat.Limit) (edgeLimit : Limit)
+    (table : List RawRat) (edges : List ArithEdge) : Result :=
+  match RationalTable.Table.check tableLimit table with
+  | .malformed index reason => .malformedTable index reason
+  | .resourceLimit index reason => .tableResource index reason
+  | .ready =>
+      if lengthWithin edgeLimit.maxEdges edges then
+        let remaining : Remaining :=
+          { lookupSteps := edgeLimit.maxLookupSteps
+            arithmeticWork := edgeLimit.maxArithmeticWork }
+        match preflightFrom edgeLimit table table.length 0 remaining edges with
+        | .ready plan => replayFrom 0 plan
+        | .failed failure => failure.result
+      else
+        .edgeResource none .edges
+
+/-- A successful replay of a related plan proves every indexed edge. -/
+theorem holds_of_replay {table : List RawRat} {edges : List ArithEdge}
+    {plan : List Resolved} {index : Nat}
+    (hc : ∀ entry ∈ table, entry.Canonical)
+    (related : Relates table edges plan)
+    (h : replayFrom index plan = .ready) :
+    ∀ edge ∈ edges, edge.Holds table := by
+  induction related generalizing index with
+  | nil => simp
+  | @cons edge edges resolved plan hresolve tail ih =>
+      unfold replayFrom at h
+      cases hcheck : resolved.check with
+      | false => simp [hcheck] at h
+      | true =>
+          simp only [hcheck, ↓reduceIte] at h
+          intro candidate hmem
+          simp only [List.mem_cons] at hmem
+          cases hmem with
+          | inl hhead =>
+              subst candidate
+              exact ⟨resolved, hresolve,
+                Resolved.sound (canonical_of_resolve hc hresolve) hcheck⟩
+          | inr htail => exact ih h candidate htail
+
+/-- Proof-facing soundness of the public checker: `ready` proves the
+mathematical meaning of every indexed edge in Core `Rat`. -/
+theorem sound_of_check {tableLimit : RawRat.Limit} {edgeLimit : Limit}
+    {table : List RawRat} {edges : List ArithEdge}
+    (h : check tableLimit edgeLimit table edges = .ready) :
+    ∀ edge ∈ edges, edge.Holds table := by
+  unfold check at h
+  cases htable : RationalTable.Table.check tableLimit table with
+  | malformed index reason => simp [htable] at h
+  | resourceLimit index reason => simp [htable] at h
+  | ready =>
+      simp only [htable] at h
+      split at h
+      next =>
+        cases hpreflight : preflightFrom edgeLimit table table.length 0
+            { lookupSteps := edgeLimit.maxLookupSteps
+              arithmeticWork := edgeLimit.maxArithmeticWork } edges with
+        | failed failure =>
+            cases failure <;> simp [hpreflight, PreflightFailure.result] at h
+        | ready plan =>
+            simp only [hpreflight] at h
+            exact holds_of_replay
+              (RationalTable.Table.canonical_of_check htable)
+              (relates_of_preflight hpreflight) h
+      next => contradiction
+
+/-! ## Fixed all-operation canaries -/
+
+/-- Canonical table used by every arithmetic-edge constructor. -/
+def fixtureTable : List RawRat :=
+  [⟨1, 2⟩, ⟨1, 3⟩, ⟨5, 6⟩, ⟨1, 6⟩, ⟨2, 1⟩]
+
+/-- Table limits with one spare slot for total zero-inverse tests. -/
+def fixtureTableLimit : RawRat.Limit :=
+  { maxEntries := 6
+    maxNumeratorBits := 8
+    maxDenominatorBits := 8 }
+
+/-- One successful edge of every first-slice operation. -/
+def fixtureEdges : List ArithEdge :=
+  [ .add 0 1 2
+  , .sub 0 1 3
+  , .mul 0 1 3
+  , .inv 0 4
+  , .eq 3 3
+  , .le 1 0
+  , .lt 1 0 ]
+
+/-- Exact conservative resource total for `fixtureEdges`: seven edges, forty
+`List` constructors visited, seven temporary bits, and 130 work units. -/
+def fixtureLimit : Limit :=
+  { maxEdges := 7
+    maxLookupSteps := 40
+    maxTemporaryBits := 7
+    maxArithmeticWork := 130 }
+
+/-- Acceptance, exact/one-over resources, complete preflight, and logical
+failure canaries for the arithmetic-edge boundary. -/
+def checksEdges : Bool :=
+  check fixtureTableLimit fixtureLimit fixtureTable fixtureEdges == .ready &&
+    check fixtureTableLimit { fixtureLimit with maxEdges := 6 }
+      fixtureTable fixtureEdges == .edgeResource none .edges &&
+    check fixtureTableLimit { fixtureLimit with maxLookupSteps := 39 }
+      fixtureTable fixtureEdges == .edgeResource (some 6) .lookupSteps &&
+    check fixtureTableLimit { fixtureLimit with maxTemporaryBits := 6 }
+      fixtureTable fixtureEdges == .edgeResource (some 0) .temporaryBits &&
+    check fixtureTableLimit { fixtureLimit with maxArithmeticWork := 129 }
+      fixtureTable fixtureEdges == .edgeResource (some 6) .arithmeticWork &&
+    check fixtureTableLimit fixtureLimit fixtureTable [.add 0 1 0] ==
+      .malformedEdge 0 .wrongIdentity &&
+    check fixtureTableLimit fixtureLimit fixtureTable [.add 0 99 2] ==
+      .malformedEdge 0 (.badIndex .right 99) &&
+    check fixtureTableLimit fixtureLimit (fixtureTable ++ [⟨0, 1⟩]) [.inv 5 5] ==
+      .ready &&
+    check fixtureTableLimit fixtureLimit fixtureTable
+      [.add 0 1 0, .mul 0 99 3] ==
+        .malformedEdge 1 (.badIndex .right 99)
+
+/-- Ordinary-kernel canary for complete arithmetic-edge validation. -/
+theorem checksEdges_eq_true : checksEdges = true := by
+  decide +kernel
+
+end Hex.Interval.Experiment.RationalEdge
diff --git a/conformance/HexInterval/RationalEdgeConformance.lean b/conformance/HexInterval/RationalEdgeConformance.lean
new file mode 100644
index 000000000..d2beaa7bc
--- /dev/null
+++ b/conformance/HexInterval/RationalEdgeConformance.lean
@@ -0,0 +1,233 @@
+/-
+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 HexInterval.Experiment.RationalEdge
+
+/-!
+Compiled conformance for resource-preflighted rational arithmetic edges.
+Ordinary-kernel examples exercise the transparent checker and every Core `Rat`
+soundness theorem from a downstream module.
+-/
+
+namespace Hex.Interval.RationalEdgeConformance
+
+open Experiment.RationalEdge
+
+#guard checksEdges
+#guard check fixtureTableLimit fixtureLimit fixtureTable fixtureEdges == .ready
+
+-- Each caller-owned resource accepts its exact fixture boundary and rejects
+-- one unit below it at the deterministic first edge that exhausts the budget.
+#guard check fixtureTableLimit { fixtureLimit with maxEdges := 6 }
+  fixtureTable fixtureEdges == .edgeResource none .edges
+#guard check fixtureTableLimit { fixtureLimit with maxLookupSteps := 40 }
+  fixtureTable fixtureEdges == .ready
+#guard check fixtureTableLimit { fixtureLimit with maxLookupSteps := 39 }
+  fixtureTable fixtureEdges == .edgeResource (some 6) .lookupSteps
+#guard check fixtureTableLimit { fixtureLimit with maxTemporaryBits := 7 }
+  fixtureTable fixtureEdges == .ready
+#guard check fixtureTableLimit { fixtureLimit with maxTemporaryBits := 6 }
+  fixtureTable fixtureEdges == .edgeResource (some 0) .temporaryBits
+#guard check fixtureTableLimit { fixtureLimit with maxArithmeticWork := 130 }
+  fixtureTable fixtureEdges == .ready
+#guard check fixtureTableLimit { fixtureLimit with maxArithmeticWork := 129 }
+  fixtureTable fixtureEdges == .edgeResource (some 6) .arithmeticWork
+
+-- Zero-aware width formulas account for every declared intermediate.  In the
+-- total inverse zero branch no cross-product or temporary is charged.
+#guard (Resolved.add ⟨0, 1⟩ ⟨1, 2⟩ ⟨1, 2⟩).cost ==
+  ({ temporaryBits := 4, arithmeticWork := 17 } : Cost)
+#guard (Resolved.mul ⟨0, 1⟩ ⟨1, 2⟩ ⟨0, 1⟩).cost ==
+  ({ temporaryBits := 3, arithmeticWork := 2 } : Cost)
+#guard (Resolved.inv ⟨0, 1⟩ ⟨0, 1⟩).cost ==
+  ({ temporaryBits := 0, arithmeticWork := 0 } : Cost)
+
+private def zeroTable : List Experiment.RationalTable.RawRat := [⟨0, 1⟩]
+
+private def zeroTableLimit : Experiment.RationalTable.RawRat.Limit :=
+  { maxEntries := 1
+    maxNumeratorBits := 0
+    maxDenominatorBits := 1 }
+
+private def zeroInvLimit : Limit :=
+  { maxEdges := 1
+    maxLookupSteps := 2
+    maxTemporaryBits := 0
+    maxArithmeticWork := 0 }
+
+#guard check zeroTableLimit zeroInvLimit zeroTable [.inv 0 0] == .ready
+
+-- No lookup defaults are accepted; inverse follows Core's total operation.
+#guard check fixtureTableLimit fixtureLimit fixtureTable [.add 0 99 2] ==
+  .malformedEdge 0 (.badIndex .right 99)
+#guard check fixtureTableLimit fixtureLimit fixtureTable [.add 99 1 2] ==
+  .malformedEdge 0 (.badIndex .left 99)
+#guard check fixtureTableLimit fixtureLimit fixtureTable [.inv 99 4] ==
+  .malformedEdge 0 (.badIndex .input 99)
+#guard check fixtureTableLimit fixtureLimit fixtureTable [.add 0 1 99] ==
+  .malformedEdge 0 (.badIndex .result 99)
+#guard check fixtureTableLimit fixtureLimit (fixtureTable ++ [⟨0, 1⟩]) [.inv 5 5] ==
+  .ready
+#guard check fixtureTableLimit fixtureLimit (fixtureTable ++ [⟨0, 1⟩]) [.inv 5 4] ==
+  .malformedEdge 0 .wrongIdentity
+#guard check fixtureTableLimit fixtureLimit fixtureTable [.add 0 1 0] ==
+  .malformedEdge 0 .wrongIdentity
+
+-- Every operation tag rejects a false assertion.
+#guard check fixtureTableLimit fixtureLimit fixtureTable [.sub 0 1 0] ==
+  .malformedEdge 0 .wrongIdentity
+#guard check fixtureTableLimit fixtureLimit fixtureTable [.mul 0 1 0] ==
+  .malformedEdge 0 .wrongIdentity
+#guard check fixtureTableLimit fixtureLimit fixtureTable [.inv 0 0] ==
+  .malformedEdge 0 .wrongIdentity
+#guard check fixtureTableLimit fixtureLimit fixtureTable [.eq 0 1] ==
+  .malformedEdge 0 .wrongIdentity
+#guard check fixtureTableLimit fixtureLimit fixtureTable [.le 0 1] ==
+  .malformedEdge 0 .wrongIdentity
+#guard check fixtureTableLimit fixtureLimit fixtureTable [.lt 0 1] ==
+  .malformedEdge 0 .wrongIdentity
+
+-- Zero arithmetic exercises zero-aware multiplication and sum widths.
+#guard check fixtureTableLimit { fixtureLimit with maxLookupSteps := 41 }
+  (fixtureTable ++ [⟨0, 1⟩])
+  [.add 5 0 0, .sub 0 0 5, .mul 5 0 5, .inv 5 5] == .ready
+
+-- Full-list preflight precedes replay: a bad later index is returned before an
+-- earlier false cross-product is ever evaluated.
+#guard check fixtureTableLimit fixtureLimit fixtureTable
+  [.add 0 1 0, .mul 0 99 3] ==
+    .malformedEdge 1 (.badIndex .right 99)
+
+-- Successful table validation remains a prerequisite of all edge work.
+#guard check fixtureTableLimit fixtureLimit
+  ([⟨1, 2⟩, ⟨2, 6⟩] : List Experiment.RationalTable.RawRat)
+  [] == .malformedTable 1 .notReduced
+#guard check { fixtureTableLimit with maxEntries := 4 } fixtureLimit
+  fixtureTable [] == .tableResource none .entries
+
+private def signedTable : List Experiment.RationalTable.RawRat :=
+  [⟨0, 1⟩, ⟨-2, 3⟩, ⟨-3, 2⟩, ⟨-1, 3⟩, ⟨-2, 3⟩]
+
+private def signedTableLimit : Experiment.RationalTable.RawRat.Limit :=
+  { maxEntries := 5
+    maxNumeratorBits := 3
+    maxDenominatorBits := 2 }
+
+private def signedLimit : Limit :=
+  { maxEdges := 5
+    maxLookupSteps := 26
+    maxTemporaryBits := 4
+    maxArithmeticWork := 50 }
+
+-- Negative inversion, equality, and both order relations use signed integer
+-- cross-products with positive canonical denominators.
+#guard check signedTableLimit signedLimit signedTable
+  [.inv 1 2, .eq 1 4, .le 1 3, .lt 1 3, .inv 0 0] == .ready
+
+private def half : Experiment.RationalTable.RawRat := ⟨1, 2⟩
+private def third : Experiment.RationalTable.RawRat := ⟨1, 3⟩
+private def fiveSixths : Experiment.RationalTable.RawRat := ⟨5, 6⟩
+private def sixth : Experiment.RationalTable.RawRat := ⟨1, 6⟩
+private def two : Experiment.RationalTable.RawRat := ⟨2, 1⟩
+private def zero : Experiment.RationalTable.RawRat := ⟨0, 1⟩
+private def negTwoThirds : Experiment.RationalTable.RawRat := ⟨-2, 3⟩
+private def negThreeHalves : Experiment.RationalTable.RawRat := ⟨-3, 2⟩
+private def negThird : Experiment.RationalTable.RawRat := ⟨-1, 3⟩
+
+private theorem halfCanonical : half.Canonical :=
+  Experiment.RationalTable.RawRat.canonical_of_check
+    (limit := fixtureTableLimit) (by decide +kernel)
+
+private theorem thirdCanonical : third.Canonical :=
+  Experiment.RationalTable.RawRat.canonical_of_check
+    (limit := fixtureTableLimit) (by decide +kernel)
+
+private theorem fiveSixthsCanonical : fiveSixths.Canonical :=
+  Experiment.RationalTable.RawRat.canonical_of_check
+    (limit := fixtureTableLimit) (by decide +kernel)
+
+private theorem sixthCanonical : sixth.Canonical :=
+  Experiment.RationalTable.RawRat.canonical_of_check
+    (limit := fixtureTableLimit) (by decide +kernel)
+
+private theorem twoCanonical : two.Canonical :=
+  Experiment.RationalTable.RawRat.canonical_of_check
+    (limit := fixtureTableLimit) (by decide +kernel)
+
+private theorem zeroCanonical : zero.Canonical :=
+  Experiment.RationalTable.RawRat.canonical_of_check
+    (limit := zeroTableLimit) (by decide +kernel)
+
+private theorem negTwoThirdsCanonical : negTwoThirds.Canonical :=
+  Experiment.RationalTable.RawRat.canonical_of_check
+    (limit := signedTableLimit) (by decide +kernel)
+
+private theorem negThreeHalvesCanonical : negThreeHalves.Canonical :=
+  Experiment.RationalTable.RawRat.canonical_of_check
+    (limit := signedTableLimit) (by decide +kernel)
+
+private theorem negThirdCanonical : negThird.Canonical :=
+  Experiment.RationalTable.RawRat.canonical_of_check
+    (limit := signedTableLimit) (by decide +kernel)
+
+-- These proofs invoke the public soundness API, rather than asking reduction
+-- to normalize Core rational arithmetic as a test oracle.
+example : fiveSixths.value = half.value + third.value := by
+  exact Resolved.add_sound halfCanonical thirdCanonical
+    fiveSixthsCanonical (by decide +kernel)
+
+example : sixth.value = half.value - third.value := by
+  exact Resolved.sub_sound halfCanonical thirdCanonical
+    sixthCanonical (by decide +kernel)
+
+example : sixth.value = half.value * third.value := by
+  exact Resolved.mul_sound halfCanonical thirdCanonical
+    sixthCanonical (by decide +kernel)
+
+example : two.value = half.value⁻¹ := by
+  exact Resolved.inv_sound halfCanonical twoCanonical
+    (by decide +kernel)
+
+example : zero.value = zero.value⁻¹ := by
+  exact Resolved.inv_sound zeroCanonical zeroCanonical (by decide +kernel)
+
+example : negThreeHalves.value = negTwoThirds.value⁻¹ := by
+  exact Resolved.inv_sound negTwoThirdsCanonical negThreeHalvesCanonical
+    (by decide +kernel)
+
+example : sixth.value = sixth.value := by
+  exact Resolved.eq_sound sixthCanonical sixthCanonical (by decide +kernel)
+
+example : third.value ≤ half.value := by
+  exact Resolved.le_sound thirdCanonical halfCanonical (by decide +kernel)
+
+example : third.value < half.value := by
+  exact Resolved.lt_sound thirdCanonical halfCanonical (by decide +kernel)
+
+example : negTwoThirds.value = negTwoThirds.value := by
+  exact Resolved.eq_sound negTwoThirdsCanonical negTwoThirdsCanonical
+    (by decide +kernel)
+
+example : negTwoThirds.value ≤ negThird.value := by
+  exact Resolved.le_sound negTwoThirdsCanonical negThirdCanonical
+    (by decide +kernel)
+
+example : negTwoThirds.value < negThird.value := by
+  exact Resolved.lt_sound negTwoThirdsCanonical negThirdCanonical
+    (by decide +kernel)
+
+-- A downstream consumer can turn public checker success directly into the
+-- indexed edge's Core `Rat` proposition.
+example : ArithEdge.Holds fixtureTable (.add 0 1 2) := by
+  have hsound := sound_of_check
+    (tableLimit := fixtureTableLimit) (edgeLimit := fixtureLimit)
+    (table := fixtureTable) (edges := fixtureEdges) (by decide +kernel)
+  exact hsound (.add 0 1 2) (by simp [fixtureEdges])
+
+example : checksEdges = true := by
+  decide +kernel
+
+end Hex.Interval.RationalEdgeConformance
diff --git a/lakefile.lean b/lakefile.lean
index 19e01c213..01c95be35 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -210,7 +210,8 @@ lean_lib HexIntervalExperiment where
   globs := #[`HexInterval.Experiment.Representation,
     `HexInterval.Experiment.Rational, `HexInterval.Experiment.Center,
     `HexInterval.Experiment.Scale, `HexInterval.Experiment.RationalTable,
-    `HexInterval.Experiment.RationalCertificate]
+    `HexInterval.Experiment.RationalCertificate,
+    `HexInterval.Experiment.RationalEdge]
 
 lean_lib HexIntervalMathlibExperiment where
   globs := #[`HexIntervalMathlib.Experiment.Center]
@@ -246,7 +247,8 @@ 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, `HexLLL.Conformance, `HexMatrix.Conformance, `HexRowReduce.Conformance, `HexDeterminant.Conformance, `HexBareiss.Conformance, `HexModArith.Conformance, `HexModArith.FastCheck, `HexPoly.Conformance, `HexPolyFp.Conformance, `HexPolyZ.Conformance, `HexRealRoots.Conformance, `HexRealRootsMathlib.Conformance, `HexRoots.Conformance] : Array Glob)
     ++ (#[`HexInterval.RationalTableConformance,
-      `HexInterval.RationalCertificateConformance] : Array Glob)
+      `HexInterval.RationalCertificateConformance,
+      `HexInterval.RationalEdgeConformance] : Array Glob)
 
 -- Public umbrellas intentionally contain only the supported API. Executable
 -- examples and regression tests are compiled through this separate target so
diff --git a/progress/20260727T105900Z.md b/progress/20260727T105900Z.md
new file mode 100644
index 000000000..39d87fcba
--- /dev/null
+++ b/progress/20260727T105900Z.md
@@ -0,0 +1,50 @@
+# Accomplished
+
+- Added `HexInterval.Experiment.RationalEdge`, a strategy-neutral, Mathlib-free
+  arithmetic-edge replay slice over canonical `RawRat` table indices.  It
+  covers addition, subtraction, multiplication, total Core rational inverse,
+  equality, non-strict order, and strict order with naive transparent integer
+  identities.
+- Added a three-phase checker: complete raw-table validation and edge-count
+  preflight; full-list index resolution and caller-owned lookup-step,
+  temporary-bit, and aggregate arithmetic-work preflight; then first-failure
+  identity replay.  No cross-product is formed before the whole edge list has
+  passed preflight, and proof-facing storage remains `List`-based.
+- Implemented the SPEC's zero-aware width model, explicit accounting for every
+  declared intermediate and final comparison, and a branch-specific zero
+  inverse cost that allocates no denominator cross-product.  Exact and
+  one-below resource canaries cover edge count, indexed-list traversal,
+  temporary width, and aggregate work.
+- Proved each resolved operation sound in Core `Rat`, including both branches
+  of `0⁻¹ = 0`, and proved the public end-to-end theorem
+  `sound_of_check`: a `ready` result establishes `ArithEdge.Holds` for every
+  indexed input edge.
+- Added compiled downstream conformance for every operation tag's false result,
+  every reference position's bad index, full-preflight-before-replay ordering,
+  signed inverse/equality/order, zero arithmetic, and a zero-inverse fixture
+  accepted with zero temporary/work budget.  Ordinary `decide +kernel`
+  exercises both the checker and proof-facing API.
+- Registered the experiment and conformance modules.  Focused module and
+  downstream builds pass, as do the import DAG check, Mathlib-free bench lint,
+  forbidden-token scan, whitespace scan, and `git diff --check`.  An axiom
+  audit reports only Lean/Core foundations (`propext`, `Classical.choice`, and
+  `Quot.sound`) for `sound_of_check`, with no `sorryAx`.
+
+# Current frontier
+
+This slice validates and proves standalone rational arithmetic edges.  It does
+not yet project an endpoint-bearing interval certificate onto those edges or
+connect a compiled Core `Rat` planner to the raw table.  Its cost policy is the
+conservative naive-cross-product baseline; cancellation-aware replay remains a
+separate experimental arm.
+
+# Next step
+
+Add the rational endpoint-bearing certificate projection and require exact
+structural-skeleton agreement with the centered dyadic arm.  Then have the
+compiled planner emit canonical raw endpoints plus these arithmetic edges and
+compare naive replay with a separately budgeted cancellation-aware candidate.
+
+# Blockers
+
+None.

From 86c3524aa5f327a702cf5b1fb093ef1477d664c1 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Mon, 27 Jul 2026 11:17:35 +0000
Subject: [PATCH 2/3] test(interval): harden rational edge replay

---
 HexInterval/Experiment/RationalEdge.lean      |  8 +++--
 .../HexInterval/RationalEdgeConformance.lean  | 19 ++++++++++++
 progress/20260727T111717Z.md                  | 30 +++++++++++++++++++
 3 files changed, 54 insertions(+), 3 deletions(-)
 create mode 100644 progress/20260727T111717Z.md

diff --git a/HexInterval/Experiment/RationalEdge.lean b/HexInterval/Experiment/RationalEdge.lean
index cb4778464..5b74d15b8 100644
--- a/HexInterval/Experiment/RationalEdge.lean
+++ b/HexInterval/Experiment/RationalEdge.lean
@@ -31,9 +31,11 @@ visited (`index + 1` for every valid reference).  Temporary widths use the
 standard conservative bounds `bits (x*y) <= bits x + bits y` and the analogous
 sum-or-difference bound `max (bits x) (bits y) + 1`.  Arithmetic work is an
 explicit schoolbook proxy: multiplying widths costs their product, and either
-adding or comparing two temporaries costs the larger width.  These formulas inspect only the bit
-lengths of already-retained inputs; they do not allocate any arithmetic
-cross-product.
+adding or comparing two temporaries costs the larger width.  The checker
+computes each edge's fixed, small aggregate from these bounded counters, then
+subtracts it from the caller-owned remaining total.  These formulas inspect
+only the bit lengths of already-retained inputs; they do not allocate any
+arithmetic cross-product.
 
 This is an experiment, not a frozen storage or certificate format.  In
 particular it adds no interval projection, wire decoder, cancellation-aware
diff --git a/conformance/HexInterval/RationalEdgeConformance.lean b/conformance/HexInterval/RationalEdgeConformance.lean
index d2beaa7bc..ad3dd131d 100644
--- a/conformance/HexInterval/RationalEdgeConformance.lean
+++ b/conformance/HexInterval/RationalEdgeConformance.lean
@@ -67,6 +67,8 @@ private def zeroInvLimit : Limit :=
   .malformedEdge 0 (.badIndex .left 99)
 #guard check fixtureTableLimit fixtureLimit fixtureTable [.inv 99 4] ==
   .malformedEdge 0 (.badIndex .input 99)
+#guard check fixtureTableLimit fixtureLimit fixtureTable [.inv 0 99] ==
+  .malformedEdge 0 (.badIndex .result 99)
 #guard check fixtureTableLimit fixtureLimit fixtureTable [.add 0 1 99] ==
   .malformedEdge 0 (.badIndex .result 99)
 #guard check fixtureTableLimit fixtureLimit (fixtureTable ++ [⟨0, 1⟩]) [.inv 5 5] ==
@@ -100,6 +102,9 @@ private def zeroInvLimit : Limit :=
 #guard check fixtureTableLimit fixtureLimit fixtureTable
   [.add 0 1 0, .mul 0 99 3] ==
     .malformedEdge 1 (.badIndex .right 99)
+#guard check fixtureTableLimit { fixtureLimit with maxTemporaryBits := 6 }
+  fixtureTable [.add 0 1 0, .add 0 1 2] ==
+    .edgeResource (some 1) .temporaryBits
 
 -- Successful table validation remains a prerequisite of all edge work.
 #guard check fixtureTableLimit fixtureLimit
@@ -127,6 +132,20 @@ private def signedLimit : Limit :=
 #guard check signedTableLimit signedLimit signedTable
   [.inv 1 2, .eq 1 4, .le 1 3, .lt 1 3, .inv 0 0] == .ready
 
+private def signedArithmeticTable : List Experiment.RationalTable.RawRat :=
+  [⟨-2, 3⟩, ⟨1, 2⟩, ⟨-1, 6⟩, ⟨-7, 6⟩, ⟨-1, 3⟩]
+
+private def signedArithmeticLimit : Limit :=
+  { maxEdges := 3
+    maxLookupSteps := 21
+    maxTemporaryBits := 8
+    maxArithmeticWork := 200 }
+
+-- Signed and mixed-sign addition, subtraction, and multiplication all replay
+-- through the same integer identities as their positive fixtures.
+#guard check fixtureTableLimit signedArithmeticLimit signedArithmeticTable
+  [.add 0 1 2, .sub 0 1 3, .mul 0 1 4] == .ready
+
 private def half : Experiment.RationalTable.RawRat := ⟨1, 2⟩
 private def third : Experiment.RationalTable.RawRat := ⟨1, 3⟩
 private def fiveSixths : Experiment.RationalTable.RawRat := ⟨5, 6⟩
diff --git a/progress/20260727T111717Z.md b/progress/20260727T111717Z.md
new file mode 100644
index 000000000..d1e6be6a9
--- /dev/null
+++ b/progress/20260727T111717Z.md
@@ -0,0 +1,30 @@
+# Accomplished
+
+- Audited the completed arithmetic-edge replay independently; all seven
+  identities, zero-aware cost formulas, full-list preflight, and the public
+  Core `Rat` soundness theorem were confirmed sound.
+- Added the missing inverse-result bad-index canary.
+- Added a later temporary-resource failure which is reported before replaying
+  an earlier false identity, complementing the existing later-index case.
+- Added signed/mixed-sign success cases for addition, subtraction, and
+  multiplication.
+- Clarified that the checker computes a fixed per-edge aggregate from bounded
+  size counters before subtracting it from the remaining arithmetic-work
+  budget; no endpoint cross-product is formed during preflight.
+
+# Current frontier
+
+The edge-specific checker is sound and its negative coverage now reaches every
+reference role and both later-preflight precedence classes.  Its inherited
+table validation still needs the separately implemented aggregate gcd budget
+before this slice is rebased and published.
+
+# Next step
+
+Rebase the edge commit and these audit fixes onto the rational gcd-budget
+slice, adapt the expanded table-limit API, and reconcile the composed SPEC's
+per-edge aggregate wording.
+
+# Blockers
+
+None.

From dd58cdaa3ffe6b14894bb1344b188a485a9eaff3 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Mon, 27 Jul 2026 11:22:42 +0000
Subject: [PATCH 3/3] fix(interval): compose rational edge budgets

---
 HexInterval/Experiment/RationalEdge.lean      |  4 ++-
 HexInterval/SPEC/hex-interval.md              | 12 ++++---
 .../HexInterval/RationalEdgeConformance.lean  | 35 +++++++++++++------
 progress/20260727T112226Z.md                  | 29 +++++++++++++++
 4 files changed, 64 insertions(+), 16 deletions(-)
 create mode 100644 progress/20260727T112226Z.md

diff --git a/HexInterval/Experiment/RationalEdge.lean b/HexInterval/Experiment/RationalEdge.lean
index 5b74d15b8..6ba2c57bc 100644
--- a/HexInterval/Experiment/RationalEdge.lean
+++ b/HexInterval/Experiment/RationalEdge.lean
@@ -782,7 +782,9 @@ def fixtureTable : List RawRat :=
 def fixtureTableLimit : RawRat.Limit :=
   { maxEntries := 6
     maxNumeratorBits := 8
-    maxDenominatorBits := 8 }
+    maxDenominatorBits := 8
+    maxGcdInputBits := 8
+    maxGcdWork := 64 }
 
 /-- One successful edge of every first-slice operation. -/
 def fixtureEdges : List ArithEdge :=
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 8c608ab89..b6038a8e0 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -370,10 +370,14 @@ corresponding expression. A separate deterministic work counter charges each
 multiplication, addition/subtraction, comparison, gcd, shift, and division.
 The initial policy may use conservative units such as
 `mulWork(x,y) = x*y`, `addWork(x,y) = max(x,y)+1`, and
-`compareWork(x,y) = max(x,y)`. It consumes one operation at a time by checking
-`cost <= remaining` and then subtracting; it never constructs an unchecked
-aggregate supplied by the certificate. These units are a stable policy and
-telemetry contract, not a claim about GMP or kernel wall time.
+`compareWork(x,y) = max(x,y)`. A checker may consume one primitive at a time,
+or compute the fixed small per-edge sum from these already bounded counters
+and check that sum against the remaining aggregate before subtracting it. The
+current naive reference arm uses the latter; the number of terms is fixed by
+the edge tag, and neither the terms nor their sum are certificate supplied. It
+never trusts an unchecked aggregate from the certificate. These units are a
+stable policy and telemetry contract, not a claim about GMP or kernel wall
+time.
 
 Whole-table canonicality has its own `maxGcdInputBits` and `maxGcdWork` caps.
 Input-size and work preflight occur before calling `Nat.gcd` for every entry,
diff --git a/conformance/HexInterval/RationalEdgeConformance.lean b/conformance/HexInterval/RationalEdgeConformance.lean
index ad3dd131d..26c44f05a 100644
--- a/conformance/HexInterval/RationalEdgeConformance.lean
+++ b/conformance/HexInterval/RationalEdgeConformance.lean
@@ -50,7 +50,9 @@ private def zeroTable : List Experiment.RationalTable.RawRat := [⟨0, 1⟩]
 private def zeroTableLimit : Experiment.RationalTable.RawRat.Limit :=
   { maxEntries := 1
     maxNumeratorBits := 0
-    maxDenominatorBits := 1 }
+    maxDenominatorBits := 1
+    maxGcdInputBits := 1
+    maxGcdWork := 1 }
 
 private def zeroInvLimit : Limit :=
   { maxEdges := 1
@@ -119,7 +121,9 @@ private def signedTable : List Experiment.RationalTable.RawRat :=
 private def signedTableLimit : Experiment.RationalTable.RawRat.Limit :=
   { maxEntries := 5
     maxNumeratorBits := 3
-    maxDenominatorBits := 2 }
+    maxDenominatorBits := 2
+    maxGcdInputBits := 2
+    maxGcdWork := 32 }
 
 private def signedLimit : Limit :=
   { maxEdges := 5
@@ -158,39 +162,48 @@ private def negThird : Experiment.RationalTable.RawRat := ⟨-1, 3⟩
 
 private theorem halfCanonical : half.Canonical :=
   Experiment.RationalTable.RawRat.canonical_of_check
-    (limit := fixtureTableLimit) (by decide +kernel)
+    (limit := fixtureTableLimit) (remainingGcdWork := fixtureTableLimit.maxGcdWork)
+    (by decide +kernel)
 
 private theorem thirdCanonical : third.Canonical :=
   Experiment.RationalTable.RawRat.canonical_of_check
-    (limit := fixtureTableLimit) (by decide +kernel)
+    (limit := fixtureTableLimit) (remainingGcdWork := fixtureTableLimit.maxGcdWork)
+    (by decide +kernel)
 
 private theorem fiveSixthsCanonical : fiveSixths.Canonical :=
   Experiment.RationalTable.RawRat.canonical_of_check
-    (limit := fixtureTableLimit) (by decide +kernel)
+    (limit := fixtureTableLimit) (remainingGcdWork := fixtureTableLimit.maxGcdWork)
+    (by decide +kernel)
 
 private theorem sixthCanonical : sixth.Canonical :=
   Experiment.RationalTable.RawRat.canonical_of_check
-    (limit := fixtureTableLimit) (by decide +kernel)
+    (limit := fixtureTableLimit) (remainingGcdWork := fixtureTableLimit.maxGcdWork)
+    (by decide +kernel)
 
 private theorem twoCanonical : two.Canonical :=
   Experiment.RationalTable.RawRat.canonical_of_check
-    (limit := fixtureTableLimit) (by decide +kernel)
+    (limit := fixtureTableLimit) (remainingGcdWork := fixtureTableLimit.maxGcdWork)
+    (by decide +kernel)
 
 private theorem zeroCanonical : zero.Canonical :=
   Experiment.RationalTable.RawRat.canonical_of_check
-    (limit := zeroTableLimit) (by decide +kernel)
+    (limit := zeroTableLimit) (remainingGcdWork := zeroTableLimit.maxGcdWork)
+    (by decide +kernel)
 
 private theorem negTwoThirdsCanonical : negTwoThirds.Canonical :=
   Experiment.RationalTable.RawRat.canonical_of_check
-    (limit := signedTableLimit) (by decide +kernel)
+    (limit := signedTableLimit) (remainingGcdWork := signedTableLimit.maxGcdWork)
+    (by decide +kernel)
 
 private theorem negThreeHalvesCanonical : negThreeHalves.Canonical :=
   Experiment.RationalTable.RawRat.canonical_of_check
-    (limit := signedTableLimit) (by decide +kernel)
+    (limit := signedTableLimit) (remainingGcdWork := signedTableLimit.maxGcdWork)
+    (by decide +kernel)
 
 private theorem negThirdCanonical : negThird.Canonical :=
   Experiment.RationalTable.RawRat.canonical_of_check
-    (limit := signedTableLimit) (by decide +kernel)
+    (limit := signedTableLimit) (remainingGcdWork := signedTableLimit.maxGcdWork)
+    (by decide +kernel)
 
 -- These proofs invoke the public soundness API, rather than asking reduction
 -- to normalize Core rational arithmetic as a test oracle.
diff --git a/progress/20260727T112226Z.md b/progress/20260727T112226Z.md
new file mode 100644
index 000000000..b4457c233
--- /dev/null
+++ b/progress/20260727T112226Z.md
@@ -0,0 +1,29 @@
+# Accomplished
+
+- Rebased the rational arithmetic-edge implementation and audit hardening onto
+  the stacked canonical-table GCD-budget slice.
+- Extended all edge conformance table policies with exact GCD input/work caps
+  and adapted downstream canonicality proofs to the explicit remaining-work
+  parameter.
+- Reconciled the SPEC with the implemented arithmetic policy: the checker may
+  compute a fixed-size per-edge aggregate solely from bounded internal counters
+  before checking and subtracting it; no certificate-supplied aggregate is
+  trusted.
+- Rebuilt the complete `HexIntervalExperiment` target plus rational edge
+  conformance, and reran line-count, import-DAG, forbidden-token, and whitespace
+  checks successfully.
+
+# Current frontier
+
+The edge checker now composes with complete-table GCD accounting and retains
+its full Core `Rat` soundness theorem.  It is ready to publish as a stacked PR
+after the local branch is pushed.
+
+# Next step
+
+Open the stacked arithmetic-edge PR, launch asynchronous Opus and CI reviews,
+then rebase the raw rational-to-dyadic projection slice on top.
+
+# Blockers
+
+None.