diff --git a/HexInterval.lean b/HexInterval.lean
index ec31fb575..bca5d7f39 100644
--- a/HexInterval.lean
+++ b/HexInterval.lean
@@ -24,7 +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, and resource-checked
+representation, resource-safe smart constructors, an explicitly unchecked
+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,
 division, and
diff --git a/HexInterval/Canonical.lean b/HexInterval/Canonical.lean
index 5ca71a5f1..aef3d5c4a 100644
--- a/HexInterval/Canonical.lean
+++ b/HexInterval/Canonical.lean
@@ -86,6 +86,66 @@ 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. 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
+  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 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
+prohibited exponent-alignment work. Ordinary untrusted endpoints must enter
+through `betweenWithin` or `ofRawWithin`.
+
+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
+    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 unchecked ordered-bounds construction exposes its exact closed cuts. -/
+@[simp]
+theorem view_ofOrderedBoundsUnchecked
+    (lower upper : Dyadic) (ordered : lower ≤ upper) :
+    (ofOrderedBoundsUnchecked lower upper ordered).view =
+      .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))
@@ -113,6 +173,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/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index ca035bd94..f2125184a 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
+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
 point.
@@ -270,6 +271,60 @@ 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`.
 
+Trusted representation decoders that already hold independently preflighted
+ordered dyadic endpoints also have a comparison-free closed constructor:
+
+```lean
+def ofOrderedBoundsUnchecked
+  (lower upper : Dyadic) (ordered : lower ≤ upper) : Interval
+
+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 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
+allocate an oversized dyadic alignment. Ordinary untrusted cuts still cross
+`ofRawWithin` or the corresponding `*Within` smart 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
 logical conjunction for the complete cut language: strict and closed ends,
@@ -332,13 +387,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` entry point 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..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
@@ -78,6 +79,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 acbcd247e..8761439c4 100644
--- a/conformance/HexInterval/Conformance.lean
+++ b/conformance/HexInterval/Conformance.lean
@@ -136,6 +136,69 @@ 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 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.ofOrderedBoundsUnchecked lower upper ordered).view =
+      .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 ==
+    finite 0 false 1 false
+
+-- 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
+  | .ready interval =>
+      interval ==
+        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)
+          (Hex.Interval.ordered_of_consistent (by decide))
+  | .resourceLimit _ => false
+
+-- 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)
+
 #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/conformance/HexIntervalMathlib/IntervalConformance.lean b/conformance/HexIntervalMathlib/IntervalConformance.lean
index 8f3c89f2a..ba5276523 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 constructor 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/20260824T100128Z.md b/progress/20260824T100128Z.md
new file mode 100644
index 000000000..58fb165a6
--- /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 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
+  `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 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.
+
+# 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.
diff --git a/progress/20260824T101457Z.md b/progress/20260824T101457Z.md
new file mode 100644
index 000000000..3b27bbee1
--- /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` 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.
+- 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 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.
+
+# Blockers
+
+None.
diff --git a/progress/20260824T102617Z.md b/progress/20260824T102617Z.md
new file mode 100644
index 000000000..4cc6e6fa2
--- /dev/null
+++ b/progress/20260824T102617Z.md
@@ -0,0 +1,41 @@
+# 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, 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.
+- Clarified that the far-endpoint canary exercises constructor totality; it
+  does not itself witness the trusted caller's separate resource preflight.
+
+# Current frontier
+
+- The trusted representation decoder has a clean-importing, theorem-backed
+  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
+
+- 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.