From 416eaa072d33409fed4eed77e87735e0cc9bd8f6 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Mon, 24 Aug 2026 10:02:05 +0000
Subject: [PATCH 1/7] feat(interval): add ordered bounds constructor

---
 HexInterval.lean                         |  3 +-
 HexInterval/Canonical.lean               | 24 +++++++++++++++
 HexInterval/SPEC/hex-interval.md         | 25 +++++++++++++--
 conformance/HexInterval/Conformance.lean | 19 ++++++++++++
 progress/20260824T100128Z.md             | 39 ++++++++++++++++++++++++
 5 files changed, 106 insertions(+), 4 deletions(-)
 create mode 100644 progress/20260824T100128Z.md

diff --git a/HexInterval.lean b/HexInterval.lean
index ec31fb575..336ba9ffc 100644
--- a/HexInterval.lean
+++ b/HexInterval.lean
@@ -24,7 +24,8 @@ public section
 data, propagation search, and replayable derivations.
 
 The public implementation exposes canonical exact intervals through a sealed
-representation, resource-safe smart constructors, and resource-checked
+representation, resource-safe smart constructors, a comparison-free closed
+constructor for already-proved ordered endpoints, and resource-checked
 intersection, hull, negation, addition, subtraction, multiplication, minimum,
 maximum, absolute value, natural power, outward regularization, reciprocal,
 division, and
diff --git a/HexInterval/Canonical.lean b/HexInterval/Canonical.lean
index 5ca71a5f1..18ade7058 100644
--- a/HexInterval/Canonical.lean
+++ b/HexInterval/Canonical.lean
@@ -86,6 +86,30 @@ def empty : Hex.Interval := .mk .empty (by rfl)
 def whole : Hex.Interval :=
   .mk (.bounds .unbounded .unbounded) (by rfl)
 
+/-- Construct a closed interval from endpoints whose order is already proved.
+
+This constructor performs no endpoint comparison. It is intended for trusted
+proof-producing boundaries that have already enforced their own resource
+limits and can supply `lower ≤ upper` without asking interval construction to
+recompute it. Untrusted endpoints must still enter through `betweenWithin` or
+`ofRawWithin`. -/
+def ofOrderedBounds (lower upper : Dyadic) (ordered : lower ≤ upper) :
+    Hex.Interval :=
+  .mk (.bounds (.finite lower false) (.finite upper false)) (by
+    simp only [Raw.CutConsistent, Raw.consistent]
+    by_cases less : lower < upper
+    · simp [less]
+    · have equal : lower = upper :=
+        Dyadic.le_antisymm ordered (Dyadic.not_le.mp less)
+      simp [equal])
+
+/-- An ordered-endpoint construction exposes exactly its closed finite cuts. -/
+@[simp]
+theorem view_ofOrderedBounds (lower upper : Dyadic) (ordered : lower ≤ upper) :
+    (ofOrderedBounds lower upper ordered).view =
+      .bounds (.finite lower false) (.finite upper false) := by
+  rfl
+
 /-- Construct a singleton after endpoint-cost preflight. -/
 def singletonWithin (limit : EndpointLimit) (value : Dyadic) : BuildResult :=
   ofRawWithin limit (.bounds (.finite value false) (.finite value false))
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index ca035bd94..2cc1ca01b 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -256,9 +256,10 @@ Internal planners and certificates may still use plain data when their own
 checked boundary authenticates it; proof traces do not inherit the public
 value's proof field.
 
-The initial supported slice exposes `view`, `empty`, `whole`, and endpoint-cost
-preflighted raw, singleton, one-sided, and finite constructors. The first
-supported operations are resource-checked intersection, hull, negation,
+The initial supported slice exposes `view`, `empty`, `whole`, endpoint-cost
+preflighted raw, singleton, one-sided, and finite constructors, and a
+proof-ordered comparison-free closed constructor. The first supported
+operations are resource-checked intersection, hull, negation,
 addition, subtraction, multiplication, minimum, maximum, absolute value,
 natural power, outward regularization, and transactional splitting at a dyadic
 point.
@@ -270,6 +271,24 @@ root `Interval` type; the 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`.
 
+Proof-producing boundaries that already hold ordered dyadic endpoints also
+have a comparison-free closed constructor:
+
+```lean
+def ofOrderedBounds (lower upper : Dyadic) (ordered : lower ≤ upper) : Interval
+
+theorem view_ofOrderedBounds (lower upper : Dyadic) (ordered : lower ≤ upper) :
+  (ofOrderedBounds lower upper ordered).view =
+    .bounds (.finite lower false) (.finite upper false)
+```
+
+This is a kernel-friendly bridge, not an untrusted decoder: it neither checks
+endpoint height nor recomputes the comparison. A projection, replay, or proof
+emitter must enforce its own resource caps before producing `ordered`.
+Untrusted cuts still cross `ofRawWithin` or the corresponding `*Within` smart
+constructor. The exact view theorem lets an importing proof consume the
+closed cuts without reducing the sealed constructor across a module boundary.
+
 The public Mathlib companion interprets every canonical interval as a subset
 of `ℝ`. It proves that a successful executable `intersectWithin` denotes
 logical conjunction for the complete cut language: strict and closed ends,
diff --git a/conformance/HexInterval/Conformance.lean b/conformance/HexInterval/Conformance.lean
index acbcd247e..82cdf6624 100644
--- a/conformance/HexInterval/Conformance.lean
+++ b/conformance/HexInterval/Conformance.lean
@@ -136,6 +136,25 @@ private def far : Dyadic := .ofOdd 1 1000000000 (by decide)
 #guard Hex.Interval.whole.view == .bounds .unbounded .unbounded
 #guard decide (Hex.Interval.empty ≠ Hex.Interval.whole)
 
+-- A proof-producing boundary can construct exact closed bounds without a
+-- second comparison. The view theorem works from this importing module, so a
+-- kernel proof does not depend on reducing the sealed constructor body.
+example (lower upper : Dyadic) (ordered : lower ≤ upper) :
+    (Hex.Interval.ofOrderedBounds lower upper ordered).view =
+      .bounds (.finite lower false) (.finite upper false) :=
+  Hex.Interval.view_ofOrderedBounds lower upper ordered
+
+#guard
+  (Hex.Interval.ofOrderedBounds (d 0) (d 1) (by decide)).view ==
+    finite 0 false 1 false
+
+-- The ordered constructor does not repeat endpoint-height or alignment work.
+-- Even a compact endpoint beyond ordinary planner caps is admitted when the
+-- caller already owns its ordering proof.
+#guard
+  (Hex.Interval.ofOrderedBounds far far (Dyadic.le_refl far)).view ==
+    .bounds (.finite far false) (.finite far false)
+
 #guard
   match Hex.Interval.betweenWithin smallLimit (d 0) false (d 1) true with
   | .ready interval => interval.view == finite 0 false 1 true
diff --git a/progress/20260824T100128Z.md b/progress/20260824T100128Z.md
new file mode 100644
index 000000000..0aa9b60af
--- /dev/null
+++ b/progress/20260824T100128Z.md
@@ -0,0 +1,39 @@
+# Accomplished
+
+- Added the Mathlib-free `Hex.Interval.ofOrderedBounds` constructor for closed
+  intervals whose dyadic endpoints arrive with a proof of `lower ≤ upper`.
+  The constructor retains the private sealed representation and performs no
+  endpoint comparison of its own.
+- Added the exact `[simp]` theorem `view_ofOrderedBounds`, allowing downstream
+  kernel proofs to recover the two closed finite cuts without reducing the
+  sealed constructor across a module boundary.
+- Added core conformance for the downstream theorem shape, an ordinary ordered
+  pair, and a compact far-exponent endpoint demonstrating that construction
+  does not repeat planner endpoint-height or alignment work.
+- Updated the HexInterval umbrella documentation and SPEC to distinguish this
+  proof-producing bridge from the resource-safe untrusted `*Within` entry
+  points. The caller remains responsible for enforcing resource caps before
+  producing the ordering proof.
+- Completed green focused builds of `HexInterval.Canonical`, `HexInterval`, and
+  `HexInterval.Conformance`, followed by a green full 10,003-job `lake build`.
+  Matching generated dependencies were reused through hard links, avoiding a
+  second physical copy while Lake rebuilt stale project outputs.
+- Completed the published trust-surface check (503 Lean files), copyright
+  headers, dependency DAG, conformance-target validation, forbidden-token
+  scan, and `git diff --check` with no failures.
+
+# Current frontier
+
+The minimal production interval-construction bridge identified by the bounded
+rational literal experiment is implemented and green. No rational term syntax,
+tactic path, Mathlib proof emitter, or runtime integration was added here.
+
+# Next step
+
+Use `ofOrderedBounds` and `view_ofOrderedBounds` from the separate rational
+term/tactic integration, after its projection caps and authenticated ordering
+proof have succeeded.
+
+# Blockers
+
+None.

From 0de2238d38b8163615df26a89b1c3b1adc5a155b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Mon, 24 Aug 2026 10:15:14 +0000
Subject: [PATCH 2/7] fix(interval): mark ordered bounds bridge unchecked

---
 HexInterval.lean                              |  5 ++-
 HexInterval/Canonical.lean                    | 28 +++++++-----
 HexInterval/SPEC/hex-interval.md              | 45 ++++++++++++-------
 HexIntervalMathlib/Interval.lean              | 10 +++++
 conformance/HexInterval/Conformance.lean      | 37 ++++++++++-----
 .../IntervalConformance.lean                  |  8 ++++
 progress/20260824T101457Z.md                  | 40 +++++++++++++++++
 7 files changed, 134 insertions(+), 39 deletions(-)
 create mode 100644 progress/20260824T101457Z.md

diff --git a/HexInterval.lean b/HexInterval.lean
index 336ba9ffc..8224ced16 100644
--- a/HexInterval.lean
+++ b/HexInterval.lean
@@ -24,8 +24,9 @@ public section
 data, propagation search, and replayable derivations.
 
 The public implementation exposes canonical exact intervals through a sealed
-representation, resource-safe smart constructors, a comparison-free closed
-constructor for already-proved ordered endpoints, and resource-checked
+representation, resource-safe smart constructors, an explicitly unchecked
+closed bridge for independently preflighted trusted representation decoders,
+and resource-checked
 intersection, hull, negation, addition, subtraction, multiplication, minimum,
 maximum, absolute value, natural power, outward regularization, reciprocal,
 division, and
diff --git a/HexInterval/Canonical.lean b/HexInterval/Canonical.lean
index 18ade7058..9127a9374 100644
--- a/HexInterval/Canonical.lean
+++ b/HexInterval/Canonical.lean
@@ -86,14 +86,19 @@ def empty : Hex.Interval := .mk .empty (by rfl)
 def whole : Hex.Interval :=
   .mk (.bounds .unbounded .unbounded) (by rfl)
 
-/-- Construct a closed interval from endpoints whose order is already proved.
-
-This constructor performs no endpoint comparison. It is intended for trusted
-proof-producing boundaries that have already enforced their own resource
-limits and can supply `lower ≤ upper` without asking interval construction to
-recompute it. Untrusted endpoints must still enter through `betweenWithin` or
-`ofRawWithin`. -/
-def ofOrderedBounds (lower upper : Dyadic) (ordered : lower ≤ upper) :
+/-- Construct a closed interval from independently preflighted ordered bounds.
+
+This is an explicitly unchecked bridge for trusted representation decoders.
+It performs no endpoint-height or comparison-cost preflight. Callers must
+preflight both costs before producing `ordered`, and must not manufacture that
+proof with an unbounded `decide`: deciding dyadic order can itself perform the
+prohibited exponent-alignment work. Ordinary untrusted endpoints must enter
+through `betweenWithin` or `ofRawWithin`.
+
+The total result lets a proof emitter quote an interval without embedding a
+module-boundary reduction proof that a `BuildResult` is ready. The caller,
+rather than the emitted term, continues to own the dynamic-range policy. -/
+def ofOrderedBoundsUnchecked (lower upper : Dyadic) (ordered : lower ≤ upper) :
     Hex.Interval :=
   .mk (.bounds (.finite lower false) (.finite upper false)) (by
     simp only [Raw.CutConsistent, Raw.consistent]
@@ -103,10 +108,11 @@ def ofOrderedBounds (lower upper : Dyadic) (ordered : lower ≤ upper) :
         Dyadic.le_antisymm ordered (Dyadic.not_le.mp less)
       simp [equal])
 
-/-- An ordered-endpoint construction exposes exactly its closed finite cuts. -/
+/-- An unchecked ordered-bounds construction exposes its exact closed cuts. -/
 @[simp]
-theorem view_ofOrderedBounds (lower upper : Dyadic) (ordered : lower ≤ upper) :
-    (ofOrderedBounds lower upper ordered).view =
+theorem view_ofOrderedBoundsUnchecked
+    (lower upper : Dyadic) (ordered : lower ≤ upper) :
+    (ofOrderedBoundsUnchecked lower upper ordered).view =
       .bounds (.finite lower false) (.finite upper false) := by
   rfl
 
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 2cc1ca01b..d7976a4e8 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -258,7 +258,7 @@ value's proof field.
 
 The initial supported slice exposes `view`, `empty`, `whole`, endpoint-cost
 preflighted raw, singleton, one-sided, and finite constructors, and a
-proof-ordered comparison-free closed constructor. The first supported
+trusted-decoder-only unchecked closed bridge. The first supported
 operations are resource-checked intersection, hull, negation,
 addition, subtraction, multiplication, minimum, maximum, absolute value,
 natural power, outward regularization, and transactional splitting at a dyadic
@@ -271,23 +271,32 @@ root `Interval` type; the 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`.
 
-Proof-producing boundaries that already hold ordered dyadic endpoints also
-have a comparison-free closed constructor:
+Trusted representation decoders that already hold independently preflighted
+ordered dyadic endpoints also have a comparison-free closed bridge:
 
 ```lean
-def ofOrderedBounds (lower upper : Dyadic) (ordered : lower ≤ upper) : Interval
+def ofOrderedBoundsUnchecked
+  (lower upper : Dyadic) (ordered : lower ≤ upper) : Interval
 
-theorem view_ofOrderedBounds (lower upper : Dyadic) (ordered : lower ≤ upper) :
-  (ofOrderedBounds lower upper ordered).view =
+theorem view_ofOrderedBoundsUnchecked
+    (lower upper : Dyadic) (ordered : lower ≤ upper) :
+  (ofOrderedBoundsUnchecked lower upper ordered).view =
     .bounds (.finite lower false) (.finite upper false)
 ```
 
-This is a kernel-friendly bridge, not an untrusted decoder: it neither checks
-endpoint height nor recomputes the comparison. A projection, replay, or proof
-emitter must enforce its own resource caps before producing `ordered`.
-Untrusted cuts still cross `ofRawWithin` or the corresponding `*Within` smart
-constructor. The exact view theorem lets an importing proof consume the
-closed cuts without reducing the sealed constructor across a module boundary.
+The `Unchecked` suffix is deliberate. This bridge neither checks endpoint
+height nor recomputes the comparison. Its trusted decoder must enforce both
+resource caps before producing `ordered`; in particular, it must not use an
+unbounded `decide` to manufacture that proof, because the decision itself may
+allocate an oversized dyadic alignment. Ordinary untrusted cuts still cross
+`ofRawWithin` or the corresponding `*Within` smart constructor.
+
+The total constructor is needed for emitted proof terms: it lets an emitter
+quote the exact interval without also quoting a kernel reduction proof that a
+`BuildResult` is ready across a module boundary. Dynamic-range policy remains
+caller-owned and is discharged before quotation. The exact view theorem then
+lets an importing proof consume the closed cuts without unfolding the sealed
+constructor.
 
 The public Mathlib companion interprets every canonical interval as a subset
 of `ℝ`. It proves that a successful executable `intersectWithin` denotes
@@ -351,13 +360,17 @@ either internal candidate. Infinite ends do not carry meaningless closure
 flags. This invariant deliberately does not claim that, for example, `(0,1)`
 contains an integer.
 
-Exact `normalizeUnchecked` is only for trusted or already-preflighted inputs: comparing
-two finite dyadics may align their exponents by shifting a mantissa. The
+Exact `normalizeUnchecked` is only for trusted or already-preflighted inputs:
+comparing two finite dyadics may align their exponents by shifting a mantissa. The
 planner-facing `normalizeWithin` first computes endpoint height and alignment
 shift from constructor fields and returns a distinct `resourceLimit` result
 when either bound is exceeded. It never interprets a refused comparison as an
-empty interval or as consistent cuts. Every future public reifier, certificate
-decoder, and planner input path must use this resource-safe entry point.
+empty interval or as consistent cuts. Every ordinary untrusted public reifier,
+certificate decoder, and planner input path must use this resource-safe entry
+point. The sole exception is a trusted representation decoder that has already
+performed the same independent endpoint-height and comparison-cost preflight;
+it may then cross an explicitly named `*Unchecked` bridge such as
+`ofOrderedBoundsUnchecked`.
 
 The representation differs from IEEE 1788 set-based intervals in one
 important respect. IEEE intervals are closed as sets of finite real numbers,
diff --git a/HexIntervalMathlib/Interval.lean b/HexIntervalMathlib/Interval.lean
index ef10ac31a..e8192e70a 100644
--- a/HexIntervalMathlib/Interval.lean
+++ b/HexIntervalMathlib/Interval.lean
@@ -78,6 +78,16 @@ def Raw.HullContains : Raw → Raw → ℝ → Prop
 /-- Mathematical membership in a canonical public interval. -/
 def Contains (interval : Hex.Interval) (x : ℝ) : Prop := interval.view.Contains x
 
+/-- Exact real membership in an independently preflighted closed-bounds
+construction. This theorem adds semantics but does not weaken the unchecked
+constructor's trusted-decoder preflight obligation. -/
+@[simp]
+theorem contains_ofOrderedBoundsUnchecked
+    (lower upper : Dyadic) (ordered : lower ≤ upper) (x : ℝ) :
+    (ofOrderedBoundsUnchecked lower upper ordered).Contains x ↔
+      toReal lower ≤ x ∧ x ≤ toReal upper := by
+  simp [Contains, Raw.Contains, Lower.Contains, Upper.Contains]
+
 theorem contains_normalize (raw : Raw) (x : ℝ) :
     raw.normalizeUnchecked.Contains x ↔ raw.Contains x := by
   cases raw with
diff --git a/conformance/HexInterval/Conformance.lean b/conformance/HexInterval/Conformance.lean
index 82cdf6624..36af3387b 100644
--- a/conformance/HexInterval/Conformance.lean
+++ b/conformance/HexInterval/Conformance.lean
@@ -136,23 +136,40 @@ private def far : Dyadic := .ofOdd 1 1000000000 (by decide)
 #guard Hex.Interval.whole.view == .bounds .unbounded .unbounded
 #guard decide (Hex.Interval.empty ≠ Hex.Interval.whole)
 
--- A proof-producing boundary can construct exact closed bounds without a
--- second comparison. The view theorem works from this importing module, so a
--- kernel proof does not depend on reducing the sealed constructor body.
+-- A trusted representation decoder can construct independently preflighted
+-- exact closed bounds without a second comparison. The view theorem works
+-- from this importing module, so a kernel proof does not depend on reducing
+-- the sealed constructor body.
 example (lower upper : Dyadic) (ordered : lower ≤ upper) :
-    (Hex.Interval.ofOrderedBounds lower upper ordered).view =
+    (Hex.Interval.ofOrderedBoundsUnchecked lower upper ordered).view =
       .bounds (.finite lower false) (.finite upper false) :=
-  Hex.Interval.view_ofOrderedBounds lower upper ordered
+  Hex.Interval.view_ofOrderedBoundsUnchecked lower upper ordered
 
 #guard
-  (Hex.Interval.ofOrderedBounds (d 0) (d 1) (by decide)).view ==
+  (Hex.Interval.ofOrderedBoundsUnchecked (d 0) (d 1) (by decide)).view ==
     finite 0 false 1 false
 
--- The ordered constructor does not repeat endpoint-height or alignment work.
--- Even a compact endpoint beyond ordinary planner caps is admitted when the
--- caller already owns its ordering proof.
+-- On admitted inputs, the unchecked trusted-decoder bridge agrees exactly
+-- with both capped public construction routes.
 #guard
-  (Hex.Interval.ofOrderedBounds far far (Dyadic.le_refl far)).view ==
+  match Hex.Interval.ofRawWithin smallLimit (finite 0 false 1 false) with
+  | .ready interval =>
+      interval ==
+        Hex.Interval.ofOrderedBoundsUnchecked (d 0) (d 1) (by decide)
+  | .resourceLimit _ => false
+
+#guard
+  match Hex.Interval.betweenWithin smallLimit (d 0) false (d 1) false with
+  | .ready interval =>
+      interval ==
+        Hex.Interval.ofOrderedBoundsUnchecked (d 0) (d 1) (by decide)
+  | .resourceLimit _ => false
+
+-- This pins only that a trusted decoder may admit a compact endpoint beyond
+-- an ordinary planner's dynamic-range cap after independent preflight. Equal
+-- endpoints make no claim about avoiding nonzero alignment work.
+#guard
+  (Hex.Interval.ofOrderedBoundsUnchecked far far (Dyadic.le_refl far)).view ==
     .bounds (.finite far false) (.finite far false)
 
 #guard
diff --git a/conformance/HexIntervalMathlib/IntervalConformance.lean b/conformance/HexIntervalMathlib/IntervalConformance.lean
index 8f3c89f2a..669574ee7 100644
--- a/conformance/HexIntervalMathlib/IntervalConformance.lean
+++ b/conformance/HexIntervalMathlib/IntervalConformance.lean
@@ -16,6 +16,14 @@ regularization, transactional split, reciprocal, and division.
 
 namespace Hex.IntervalMathlib.Conformance
 
+/-- The trusted-decoder bridge has the exact closed real membership promised
+by its raw view theorem. -/
+theorem orderedBoundsUncheckedExact
+    (lower upper : Dyadic) (ordered : lower ≤ upper) (x : ℝ) :
+    (Hex.Interval.ofOrderedBoundsUnchecked lower upper ordered).Contains x ↔
+      Hex.Interval.toReal lower ≤ x ∧ x ≤ Hex.Interval.toReal upper :=
+  Hex.Interval.contains_ofOrderedBoundsUnchecked lower upper ordered x
+
 /-- Both input membership proofs are required to establish membership in a
 successful public intersection. -/
 theorem intersectMember {limit : Hex.Interval.EndpointLimit}
diff --git a/progress/20260824T101457Z.md b/progress/20260824T101457Z.md
new file mode 100644
index 000000000..5ae6c5f6c
--- /dev/null
+++ b/progress/20260824T101457Z.md
@@ -0,0 +1,40 @@
+# Accomplished
+
+- Renamed the trusted representation-decoder API to the explicit
+  `ofOrderedBoundsUnchecked` and `view_ofOrderedBoundsUnchecked` vocabulary.
+- Strengthened the constructor documentation: callers must independently
+  preflight endpoint height and comparison cost, and must not manufacture the
+  ordering proof through an unbounded `decide` that could itself allocate an
+  oversized dyadic alignment.
+- Reconciled the SPEC's resource-boundary rule. Ordinary untrusted reifiers,
+  certificate decoders, and planner inputs remain on capped `*Within` entry
+  points; only independently preflighted trusted representation decoders may
+  use explicitly named `*Unchecked` bridges.
+- Documented why emitted proof terms need a total interval constructor while
+  dynamic-range policy remains owned and discharged by the caller before
+  quotation.
+- Added core canaries showing exact agreement with both `ofRawWithin` and
+  `betweenWithin` on admitted closed bounds. Corrected the far-endpoint canary
+  to claim only trusted admission beyond an ordinary planner's dynamic-range
+  cap, not avoided alignment work.
+- Added the clean Mathlib-layer theorem
+  `contains_ofOrderedBoundsUnchecked` and downstream conformance for its exact
+  closed real membership semantics.
+- Completed green focused core/Mathlib conformance builds and a green full
+  10,003-job `lake build`, plus published trust-surface, copyright, dependency
+  DAG, conformance-target, forbidden-token, and whitespace checks.
+
+# Current frontier
+
+The review-requested trust vocabulary and policy clarification are complete on
+PR #9529's branch. The branch contains no rational literal or tactic wiring.
+
+# Next step
+
+Use the explicitly unchecked bridge only after the rational projection path
+has independently enforced endpoint and comparison caps, then quote its view
+and membership theorems through the authenticated proof emitter.
+
+# Blockers
+
+None.

From 89905f36c827edfa3f5ac1f50cf77cbadeefb888 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Mon, 24 Aug 2026 10:26:34 +0000
Subject: [PATCH 3/7] fix(interval): close ordered-bounds decoder contract

---
 HexInterval/Canonical.lean               | 25 +++++++++++++++++
 HexIntervalMathlib/Interval.lean         |  1 +
 conformance/HexInterval/Conformance.lean |  9 ++++---
 progress/20260824T102617Z.md             | 34 ++++++++++++++++++++++++
 4 files changed, 66 insertions(+), 3 deletions(-)
 create mode 100644 progress/20260824T102617Z.md

diff --git a/HexInterval/Canonical.lean b/HexInterval/Canonical.lean
index 9127a9374..b3eb39fbb 100644
--- a/HexInterval/Canonical.lean
+++ b/HexInterval/Canonical.lean
@@ -86,6 +86,19 @@ def empty : Hex.Interval := .mk .empty (by rfl)
 def whole : Hex.Interval :=
   .mk (.bounds .unbounded .unbounded) (by rfl)
 
+/-- Closed consistent finite cuts recover the endpoint order needed by trusted
+representation decoders. This consumes an existing kernel proof; it performs
+no executable dyadic comparison. -/
+theorem ordered_of_consistent {lower upper : Dyadic}
+    (h : (Raw.bounds (.finite lower false) (.finite upper false)).CutConsistent) :
+    lower ≤ upper := by
+  by_cases less : lower < upper
+  · rw [← Dyadic.toRat_le_toRat_iff]
+    exact Rat.le_of_lt (Dyadic.toRat_lt_toRat_iff.mpr less)
+  · by_cases equal : lower = upper
+    · exact equal ▸ Dyadic.le_refl lower
+    · simp [Raw.CutConsistent, Raw.consistent, less, equal] at h
+
 /-- Construct a closed interval from independently preflighted ordered bounds.
 
 This is an explicitly unchecked bridge for trusted representation decoders.
@@ -116,6 +129,18 @@ theorem view_ofOrderedBoundsUnchecked
       .bounds (.finite lower false) (.finite upper false) := by
   rfl
 
+/-- Whenever the checked raw constructor admits already-consistent closed
+bounds, it returns exactly the unchecked trusted-decoder construction. -/
+theorem eq_ordered_ofRawWithin {limit : EndpointLimit} {lower upper : Dyadic}
+    {interval : Hex.Interval} (ordered : lower ≤ upper)
+    (h : ofRawWithin limit
+      (.bounds (.finite lower false) (.finite upper false)) = .ready interval) :
+    interval = ofOrderedBoundsUnchecked lower upper ordered := by
+  apply ext
+  rw [view_ofRawWithin_ready h, view_ofOrderedBoundsUnchecked]
+  apply Raw.normalizeUnchecked_eq_self
+  exact view_consistent (ofOrderedBoundsUnchecked lower upper ordered)
+
 /-- Construct a singleton after endpoint-cost preflight. -/
 def singletonWithin (limit : EndpointLimit) (value : Dyadic) : BuildResult :=
   ofRawWithin limit (.bounds (.finite value false) (.finite value false))
diff --git a/HexIntervalMathlib/Interval.lean b/HexIntervalMathlib/Interval.lean
index e8192e70a..f8474f379 100644
--- a/HexIntervalMathlib/Interval.lean
+++ b/HexIntervalMathlib/Interval.lean
@@ -9,6 +9,7 @@ module
 public import Mathlib.Data.Rat.Cast.Order
 public import Mathlib.Data.Real.Basic
 public import Mathlib.Tactic.Linarith
+public import HexInterval.Canonical
 public import HexInterval.Interval
 
 @[expose] public section
diff --git a/conformance/HexInterval/Conformance.lean b/conformance/HexInterval/Conformance.lean
index 36af3387b..902cc9adb 100644
--- a/conformance/HexInterval/Conformance.lean
+++ b/conformance/HexInterval/Conformance.lean
@@ -146,7 +146,8 @@ example (lower upper : Dyadic) (ordered : lower ≤ upper) :
   Hex.Interval.view_ofOrderedBoundsUnchecked lower upper ordered
 
 #guard
-  (Hex.Interval.ofOrderedBoundsUnchecked (d 0) (d 1) (by decide)).view ==
+  (Hex.Interval.ofOrderedBoundsUnchecked (d 0) (d 1)
+    (Hex.Interval.ordered_of_consistent (by decide))).view ==
     finite 0 false 1 false
 
 -- On admitted inputs, the unchecked trusted-decoder bridge agrees exactly
@@ -155,14 +156,16 @@ example (lower upper : Dyadic) (ordered : lower ≤ upper) :
   match Hex.Interval.ofRawWithin smallLimit (finite 0 false 1 false) with
   | .ready interval =>
       interval ==
-        Hex.Interval.ofOrderedBoundsUnchecked (d 0) (d 1) (by decide)
+        Hex.Interval.ofOrderedBoundsUnchecked (d 0) (d 1)
+          (Hex.Interval.ordered_of_consistent (by decide))
   | .resourceLimit _ => false
 
 #guard
   match Hex.Interval.betweenWithin smallLimit (d 0) false (d 1) false with
   | .ready interval =>
       interval ==
-        Hex.Interval.ofOrderedBoundsUnchecked (d 0) (d 1) (by decide)
+        Hex.Interval.ofOrderedBoundsUnchecked (d 0) (d 1)
+          (Hex.Interval.ordered_of_consistent (by decide))
   | .resourceLimit _ => false
 
 -- This pins only that a trusted decoder may admit a compact endpoint beyond
diff --git a/progress/20260824T102617Z.md b/progress/20260824T102617Z.md
new file mode 100644
index 000000000..505055628
--- /dev/null
+++ b/progress/20260824T102617Z.md
@@ -0,0 +1,34 @@
+# Accomplished
+
+- Rebuilt the ordered-bounds constructor through a clean consumer path and
+  found that the Mathlib semantics module depended on a stale transitive
+  import. It now imports `HexInterval.Canonical` directly.
+- Added `ordered_of_consistent`, which recovers endpoint order from an existing
+  closed-cut consistency proof without running an executable dyadic
+  comparison.
+- Added the general `eq_ordered_ofRawWithin` agreement theorem between a
+  successful checked raw construction and the trusted ordered-bounds
+  constructor. Conformance examples now obtain order through the consistency
+  theorem rather than presenting an unqualified `by decide` as the public
+  usage pattern.
+- Rebuilt `HexInterval.Canonical`, `HexIntervalMathlib.Interval`, and
+  `HexInterval.Conformance`; the DAG, copyright, trust-surface, prohibited-term,
+  and diff checks pass.
+
+# Current frontier
+
+- The trusted representation decoder has a clean-importing, theorem-backed
+  route from independently checked closed cuts to the exact public interval.
+- The raw-token rational experiment is consuming this route through the typed
+  runtime while production tactic behavior remains unchanged.
+
+# Next step
+
+- Push the strengthened exact head, wait for replacement CI, and obtain the
+  final independent review before merging the ordered-bounds API.
+- Complete the rational experiment's exact initial-context and final-output
+  quotation, then promote the successful shape into the production stack.
+
+# Blockers
+
+- No soundness, typing, or representation blocker is known.

From 59a9ee275402788c0b4962e413c491115d80b62c Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Mon, 24 Aug 2026 10:40:03 +0000
Subject: [PATCH 4/7] test(interval): pin ordered-bounds agreement

---
 HexInterval/Canonical.lean               | 12 +++++++++++-
 conformance/HexInterval/Conformance.lean | 23 +++++++++++++++++++++++
 progress/20260824T102617Z.md             |  8 +++++---
 3 files changed, 39 insertions(+), 4 deletions(-)

diff --git a/HexInterval/Canonical.lean b/HexInterval/Canonical.lean
index b3eb39fbb..d9ea35530 100644
--- a/HexInterval/Canonical.lean
+++ b/HexInterval/Canonical.lean
@@ -88,7 +88,9 @@ def whole : Hex.Interval :=
 
 /-- Closed consistent finite cuts recover the endpoint order needed by trusted
 representation decoders. This consumes an existing kernel proof; it performs
-no executable dyadic comparison. -/
+no executable dyadic comparison. The theorem does not make construction of
+`h` cost-free: untrusted decoders must obtain it from their independently
+bounded comparison proof, not from an unbounded decision procedure. -/
 theorem ordered_of_consistent {lower upper : Dyadic}
     (h : (Raw.bounds (.finite lower false) (.finite upper false)).CutConsistent) :
     lower ≤ upper := by
@@ -168,6 +170,14 @@ def betweenWithin (limit : EndpointLimit)
   ofRawWithin limit
     (.bounds (.finite lower lowerStrict) (.finite upper upperStrict))
 
+/-- A successful checked closed finite constructor agrees with the unchecked
+trusted-decoder construction on the same independently proved order. -/
+theorem eq_ordered_of_betweenWithin {limit : EndpointLimit} {lower upper : Dyadic}
+    {interval : Hex.Interval} (ordered : lower ≤ upper)
+    (h : betweenWithin limit lower false upper false = .ready interval) :
+    interval = ofOrderedBoundsUnchecked lower upper ordered :=
+  eq_ordered_ofRawWithin ordered h
+
 @[simp]
 theorem view_empty : empty.view = .empty := by rfl
 
diff --git a/conformance/HexInterval/Conformance.lean b/conformance/HexInterval/Conformance.lean
index 902cc9adb..25577480c 100644
--- a/conformance/HexInterval/Conformance.lean
+++ b/conformance/HexInterval/Conformance.lean
@@ -145,6 +145,29 @@ example (lower upper : Dyadic) (ordered : lower ≤ upper) :
       .bounds (.finite lower false) (.finite upper false) :=
   Hex.Interval.view_ofOrderedBoundsUnchecked lower upper ordered
 
+-- A decoder that already proved the corresponding rational inequality can
+-- transport that proof to dyadics without executing another comparison.
+example (lower upper : Dyadic) (orderedRat : lower.toRat ≤ upper.toRat) :
+    lower ≤ upper :=
+  Dyadic.toRat_le_toRat_iff.mp orderedRat
+
+-- Pin both general checked/unchecked agreement contracts at the importing
+-- boundary, independently of the concrete executable canaries below.
+example {limit : EndpointLimit} {lower upper : Dyadic} {interval : Hex.Interval}
+    (ordered : lower ≤ upper)
+    (checked : Hex.Interval.ofRawWithin limit
+      (.bounds (.finite lower false) (.finite upper false)) = .ready interval) :
+    interval = Hex.Interval.ofOrderedBoundsUnchecked lower upper ordered :=
+  Hex.Interval.eq_ordered_ofRawWithin ordered checked
+
+example {limit : EndpointLimit} {lower upper : Dyadic} {interval : Hex.Interval}
+    (ordered : lower ≤ upper)
+    (checked : Hex.Interval.betweenWithin limit lower false upper false = .ready interval) :
+    interval = Hex.Interval.ofOrderedBoundsUnchecked lower upper ordered :=
+  Hex.Interval.eq_ordered_of_betweenWithin ordered checked
+
+-- The following decisions are deliberately tiny literal canaries, not the
+-- trusted-decoder pattern for arbitrary endpoints.
 #guard
   (Hex.Interval.ofOrderedBoundsUnchecked (d 0) (d 1)
     (Hex.Interval.ordered_of_consistent (by decide))).view ==
diff --git a/progress/20260824T102617Z.md b/progress/20260824T102617Z.md
index 505055628..a04e7bdc1 100644
--- a/progress/20260824T102617Z.md
+++ b/progress/20260824T102617Z.md
@@ -8,9 +8,11 @@
   comparison.
 - Added the general `eq_ordered_ofRawWithin` agreement theorem between a
   successful checked raw construction and the trusted ordered-bounds
-  constructor. Conformance examples now obtain order through the consistency
-  theorem rather than presenting an unqualified `by decide` as the public
-  usage pattern.
+  constructor, plus the corresponding `betweenWithin` agreement theorem.
+  Conformance now pins both general contracts and demonstrates transporting an
+  already-proved rational inequality without re-running dyadic comparison;
+  the remaining decisions are explicitly tiny literal canaries rather than a
+  decoder usage pattern.
 - Rebuilt `HexInterval.Canonical`, `HexIntervalMathlib.Interval`, and
   `HexInterval.Conformance`; the DAG, copyright, trust-surface, prohibited-term,
   and diff checks pass.

From 265d7a08baa43cb1e86de9aa8504654255503550 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Mon, 24 Aug 2026 10:45:53 +0000
Subject: [PATCH 5/7] docs(interval): state opaque replay boundary

---
 HexInterval/Canonical.lean       |  9 ++++++---
 HexInterval/SPEC/hex-interval.md | 20 ++++++++++++++------
 progress/20260824T102617Z.md     |  9 ++++++---
 3 files changed, 26 insertions(+), 12 deletions(-)

diff --git a/HexInterval/Canonical.lean b/HexInterval/Canonical.lean
index d9ea35530..26bd5fe6c 100644
--- a/HexInterval/Canonical.lean
+++ b/HexInterval/Canonical.lean
@@ -110,9 +110,12 @@ proof with an unbounded `decide`: deciding dyadic order can itself perform the
 prohibited exponent-alignment work. Ordinary untrusted endpoints must enter
 through `betweenWithin` or `ofRawWithin`.
 
-The total result lets a proof emitter quote an interval without embedding a
-module-boundary reduction proof that a `BuildResult` is ready. The caller,
-rather than the emitted term, continues to own the dynamic-range policy. -/
+The total result lets a semantic proof emitter quote an interval without
+embedding a module-boundary reduction proof that a `BuildResult` is ready. The
+caller, rather than the emitted term, continues to own the dynamic-range
+policy. The constructor remains opaque outside this module: its view theorem
+supports propositional rewriting, but it deliberately does not make
+`DecidableEq`-based replay reduce through the sealed representation. -/
 def ofOrderedBoundsUnchecked (lower upper : Dyadic) (ordered : lower ≤ upper) :
     Hex.Interval :=
   .mk (.bounds (.finite lower false) (.finite upper false)) (by
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index d7976a4e8..7929ad071 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -291,12 +291,20 @@ unbounded `decide` to manufacture that proof, because the decision itself may
 allocate an oversized dyadic alignment. Ordinary untrusted cuts still cross
 `ofRawWithin` or the corresponding `*Within` smart constructor.
 
-The total constructor is needed for emitted proof terms: it lets an emitter
-quote the exact interval without also quoting a kernel reduction proof that a
-`BuildResult` is ready across a module boundary. Dynamic-range policy remains
-caller-owned and is discharged before quotation. The exact view theorem then
-lets an importing proof consume the closed cuts without unfolding the sealed
-constructor.
+The total constructor is needed for emitted semantic proof terms: it lets an
+emitter quote the exact interval without also quoting a kernel reduction proof
+that a `BuildResult` is ready across a module boundary. Dynamic-range policy
+remains caller-owned and is discharged before quotation. The exact view
+theorem then lets an importing proof consume the closed cuts without unfolding
+the sealed constructor.
+
+This is a propositional quotation boundary, not a transparent executable
+encoding. The constructor remains opaque because its body uses the sealed
+private representation. A generic replay path whose `DecidableEq Interval`
+must reduce quoted facts therefore cannot compute through this constructor;
+such a path needs a separate kernel proof of the exact initial target/fact
+correspondence rather than treating the view theorem as definitional
+reduction.
 
 The public Mathlib companion interprets every canonical interval as a subset
 of `ℝ`. It proves that a successful executable `intersectWithin` denotes
diff --git a/progress/20260824T102617Z.md b/progress/20260824T102617Z.md
index a04e7bdc1..604139521 100644
--- a/progress/20260824T102617Z.md
+++ b/progress/20260824T102617Z.md
@@ -20,9 +20,12 @@
 # Current frontier
 
 - The trusted representation decoder has a clean-importing, theorem-backed
-  route from independently checked closed cuts to the exact public interval.
-- The raw-token rational experiment is consuming this route through the typed
-  runtime while production tactic behavior remains unchanged.
+  route from independently checked closed cuts to the exact public interval
+  for semantic proof quotation.
+- The raw-token rational experiment confirmed that the opaque constructor does
+  not make generic `DecidableEq` replay computationally reducible. A separate
+  exact initial-target evidence path is being tested; production tactic
+  behavior remains unchanged.
 
 # Next step
 

From d6806183e598afca415394d3dab7c593ae667601 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Mon, 24 Aug 2026 10:57:50 +0000
Subject: [PATCH 6/7] fix interval: complete ordered-bounds contract

---
 HexInterval.lean                              |  2 +-
 HexInterval/Canonical.lean                    |  2 +-
 HexInterval/SPEC/hex-interval.md              | 27 ++++++++++++++++---
 conformance/HexInterval/Conformance.lean      |  2 +-
 .../IntervalConformance.lean                  |  2 +-
 progress/20260824T100128Z.md                  |  4 +--
 progress/20260824T101457Z.md                  |  4 +--
 7 files changed, 31 insertions(+), 12 deletions(-)

diff --git a/HexInterval.lean b/HexInterval.lean
index 8224ced16..bca5d7f39 100644
--- a/HexInterval.lean
+++ b/HexInterval.lean
@@ -25,7 +25,7 @@ data, propagation search, and replayable derivations.
 
 The public implementation exposes canonical exact intervals through a sealed
 representation, resource-safe smart constructors, an explicitly unchecked
-closed bridge for independently preflighted trusted representation decoders,
+closed constructor for independently preflighted trusted representation decoders,
 and resource-checked
 intersection, hull, negation, addition, subtraction, multiplication, minimum,
 maximum, absolute value, natural power, outward regularization, reciprocal,
diff --git a/HexInterval/Canonical.lean b/HexInterval/Canonical.lean
index 26bd5fe6c..aef3d5c4a 100644
--- a/HexInterval/Canonical.lean
+++ b/HexInterval/Canonical.lean
@@ -103,7 +103,7 @@ theorem ordered_of_consistent {lower upper : Dyadic}
 
 /-- Construct a closed interval from independently preflighted ordered bounds.
 
-This is an explicitly unchecked bridge for trusted representation decoders.
+This is an explicitly unchecked constructor for trusted representation decoders.
 It performs no endpoint-height or comparison-cost preflight. Callers must
 preflight both costs before producing `ordered`, and must not manufacture that
 proof with an unbounded `decide`: deciding dyadic order can itself perform the
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 7929ad071..f2125184a 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -258,7 +258,7 @@ value's proof field.
 
 The initial supported slice exposes `view`, `empty`, `whole`, endpoint-cost
 preflighted raw, singleton, one-sided, and finite constructors, and a
-trusted-decoder-only unchecked closed bridge. The first supported
+trusted-decoder-only unchecked closed constructor. The first supported
 operations are resource-checked intersection, hull, negation,
 addition, subtraction, multiplication, minimum, maximum, absolute value,
 natural power, outward regularization, and transactional splitting at a dyadic
@@ -272,7 +272,7 @@ if qualification proves awkward. Unless a block explicitly says otherwise,
 unqualified API sketches below are declarations inside `Hex.Interval`.
 
 Trusted representation decoders that already hold independently preflighted
-ordered dyadic endpoints also have a comparison-free closed bridge:
+ordered dyadic endpoints also have a comparison-free closed constructor:
 
 ```lean
 def ofOrderedBoundsUnchecked
@@ -282,9 +282,28 @@ theorem view_ofOrderedBoundsUnchecked
     (lower upper : Dyadic) (ordered : lower ≤ upper) :
   (ofOrderedBoundsUnchecked lower upper ordered).view =
     .bounds (.finite lower false) (.finite upper false)
+
+theorem ordered_of_consistent
+    {lower upper : Dyadic}
+    (h : (Raw.bounds (.finite lower false)
+      (.finite upper false)).CutConsistent) :
+  lower ≤ upper
+
+theorem eq_ordered_ofRawWithin
+    {limit : EndpointLimit} {lower upper : Dyadic} {interval : Interval}
+    (ordered : lower ≤ upper)
+    (h : ofRawWithin limit
+      (.bounds (.finite lower false) (.finite upper false)) = .ready interval) :
+  interval = ofOrderedBoundsUnchecked lower upper ordered
+
+theorem eq_ordered_of_betweenWithin
+    {limit : EndpointLimit} {lower upper : Dyadic} {interval : Interval}
+    (ordered : lower ≤ upper)
+    (h : betweenWithin limit lower false upper false = .ready interval) :
+  interval = ofOrderedBoundsUnchecked lower upper ordered
 ```
 
-The `Unchecked` suffix is deliberate. This bridge neither checks endpoint
+The `Unchecked` suffix is deliberate. This constructor neither checks endpoint
 height nor recomputes the comparison. Its trusted decoder must enforce both
 resource caps before producing `ordered`; in particular, it must not use an
 unbounded `decide` to manufacture that proof, because the decision itself may
@@ -377,7 +396,7 @@ empty interval or as consistent cuts. Every ordinary untrusted public reifier,
 certificate decoder, and planner input path must use this resource-safe entry
 point. The sole exception is a trusted representation decoder that has already
 performed the same independent endpoint-height and comparison-cost preflight;
-it may then cross an explicitly named `*Unchecked` bridge such as
+it may then cross an explicitly named `*Unchecked` entry point such as
 `ofOrderedBoundsUnchecked`.
 
 The representation differs from IEEE 1788 set-based intervals in one
diff --git a/conformance/HexInterval/Conformance.lean b/conformance/HexInterval/Conformance.lean
index 25577480c..13a8944b3 100644
--- a/conformance/HexInterval/Conformance.lean
+++ b/conformance/HexInterval/Conformance.lean
@@ -173,7 +173,7 @@ example {limit : EndpointLimit} {lower upper : Dyadic} {interval : Hex.Interval}
     (Hex.Interval.ordered_of_consistent (by decide))).view ==
     finite 0 false 1 false
 
--- On admitted inputs, the unchecked trusted-decoder bridge agrees exactly
+-- On admitted inputs, the unchecked trusted-decoder constructor agrees exactly
 -- with both capped public construction routes.
 #guard
   match Hex.Interval.ofRawWithin smallLimit (finite 0 false 1 false) with
diff --git a/conformance/HexIntervalMathlib/IntervalConformance.lean b/conformance/HexIntervalMathlib/IntervalConformance.lean
index 669574ee7..ba5276523 100644
--- a/conformance/HexIntervalMathlib/IntervalConformance.lean
+++ b/conformance/HexIntervalMathlib/IntervalConformance.lean
@@ -16,7 +16,7 @@ regularization, transactional split, reciprocal, and division.
 
 namespace Hex.IntervalMathlib.Conformance
 
-/-- The trusted-decoder bridge has the exact closed real membership promised
+/-- The trusted-decoder constructor has the exact closed real membership promised
 by its raw view theorem. -/
 theorem orderedBoundsUncheckedExact
     (lower upper : Dyadic) (ordered : lower ≤ upper) (x : ℝ) :
diff --git a/progress/20260824T100128Z.md b/progress/20260824T100128Z.md
index 0aa9b60af..58fb165a6 100644
--- a/progress/20260824T100128Z.md
+++ b/progress/20260824T100128Z.md
@@ -11,7 +11,7 @@
   pair, and a compact far-exponent endpoint demonstrating that construction
   does not repeat planner endpoint-height or alignment work.
 - Updated the HexInterval umbrella documentation and SPEC to distinguish this
-  proof-producing bridge from the resource-safe untrusted `*Within` entry
+  proof-producing constructor from the resource-safe untrusted `*Within` entry
   points. The caller remains responsible for enforcing resource caps before
   producing the ordering proof.
 - Completed green focused builds of `HexInterval.Canonical`, `HexInterval`, and
@@ -24,7 +24,7 @@
 
 # Current frontier
 
-The minimal production interval-construction bridge identified by the bounded
+The minimal production interval-construction API identified by the bounded
 rational literal experiment is implemented and green. No rational term syntax,
 tactic path, Mathlib proof emitter, or runtime integration was added here.
 
diff --git a/progress/20260824T101457Z.md b/progress/20260824T101457Z.md
index 5ae6c5f6c..3b27bbee1 100644
--- a/progress/20260824T101457Z.md
+++ b/progress/20260824T101457Z.md
@@ -9,7 +9,7 @@
 - Reconciled the SPEC's resource-boundary rule. Ordinary untrusted reifiers,
   certificate decoders, and planner inputs remain on capped `*Within` entry
   points; only independently preflighted trusted representation decoders may
-  use explicitly named `*Unchecked` bridges.
+  use explicitly named `*Unchecked` entry points.
 - Documented why emitted proof terms need a total interval constructor while
   dynamic-range policy remains owned and discharged by the caller before
   quotation.
@@ -31,7 +31,7 @@ PR #9529's branch. The branch contains no rational literal or tactic wiring.
 
 # Next step
 
-Use the explicitly unchecked bridge only after the rational projection path
+Use the explicitly unchecked constructor only after the rational projection path
 has independently enforced endpoint and comparison caps, then quote its view
 and membership theorems through the authenticated proof emitter.
 

From f8a59199fe5838e87bafca4322be046adce2e0df Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Mon, 24 Aug 2026 11:10:36 +0000
Subject: [PATCH 7/7] docs(interval): separate constructor canary from
 preflight

---
 conformance/HexInterval/Conformance.lean | 7 ++++---
 progress/20260824T102617Z.md             | 2 ++
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/conformance/HexInterval/Conformance.lean b/conformance/HexInterval/Conformance.lean
index 13a8944b3..8761439c4 100644
--- a/conformance/HexInterval/Conformance.lean
+++ b/conformance/HexInterval/Conformance.lean
@@ -191,9 +191,10 @@ example {limit : EndpointLimit} {lower upper : Dyadic} {interval : Hex.Interval}
           (Hex.Interval.ordered_of_consistent (by decide))
   | .resourceLimit _ => false
 
--- This pins only that a trusted decoder may admit a compact endpoint beyond
--- an ordinary planner's dynamic-range cap after independent preflight. Equal
--- endpoints make no claim about avoiding nonzero alignment work.
+-- This pins only that the constructor itself accepts a compact endpoint beyond
+-- an ordinary planner's dynamic-range cap. The trusted caller's independent
+-- preflight is a separate obligation. Equal endpoints make no claim about
+-- avoiding nonzero alignment work.
 #guard
   (Hex.Interval.ofOrderedBoundsUnchecked far far (Dyadic.le_refl far)).view ==
     .bounds (.finite far false) (.finite far false)
diff --git a/progress/20260824T102617Z.md b/progress/20260824T102617Z.md
index 604139521..4cc6e6fa2 100644
--- a/progress/20260824T102617Z.md
+++ b/progress/20260824T102617Z.md
@@ -16,6 +16,8 @@
 - Rebuilt `HexInterval.Canonical`, `HexIntervalMathlib.Interval`, and
   `HexInterval.Conformance`; the DAG, copyright, trust-surface, prohibited-term,
   and diff checks pass.
+- Clarified that the far-endpoint canary exercises constructor totality; it
+  does not itself witness the trusted caller's separate resource preflight.
 
 # Current frontier