Refinement Geometry — speculative

docs/refinement-geometry.md

Status: B (analytical, unimplemented, untested). Refereed — no novel theorem. An internal referee pass concluded that every surviving statement is either a known theorem transferred, an immediate consequence of one, or a correction of an error this programme introduced. The work is a novel synthesis with no novel theorem: a coherent application of quantitative domain theory to evidence-based refinement. It is a contribution to the design question, not to domain theory. See §Referee findings. Kept separate from foundation.md and verification-theory.md, which record measured findings. Nothing here has been executed against this repository, and by the fixed point recorded in this investigation, analytical results in this program have a poor survival rate. Read accordingly.

Setting

A refinement order R with an injective monotone evidence embedding E : R ↪ 𝒫(𝓔).

Representation Theorem

The following are equivalent:

R admits a faithful real-valued isotone representation μ.
R admits a countable separating family of down-sets: for all x ⊏ y there is a down-closed D with x ∈ D, y ∉ D. (Richter 1966, Peleg 1970, Herden 1989.)

There is a faithful Lawvere quasi-metric

d(x,y) = Σ_{e ∈ E(y)\E(x)} wₑ   for x ⊑ y,   ∞ otherwise.

(2)⟹(1): μ(x) = Σᵢ wᵢ·[x ∉ Dᵢ] with Σwᵢ < ∞. Monotone since each Dᵢ is down-closed; faithful since separation contributes a positive term. (1)⟹(2): take D_q = {x : μ(x) < q} for rational q. (1)⟺(3): the triangle inequality holds with equality along chains and vacuously off them.

Corollary. If 𝓔 is countable, (2) holds automatically: take Dₑ = {x : e ∉ E(x)}, down-closed, separating by injectivity of E, one per atom. Any system that records its evidence has countable evidence, so the hypothesis describes recording rather than restricting it.

Uniqueness. Adding chain additivity — d(x,z) = d(x,y) + d(y,z) for x ⊑ y ⊑ z — and evidence locality — d depends only on E(y)\E(x) — forces the sum form above, unique up to the weights {wₑ}.

Two open technical points

The step from finite additivity to a sum over atoms needs countable additivity when evidence differences are infinite. Finite differences suffice, and every recorded refinement step adds finitely much, but this is a hypothesis rather than a consequence.
The theorem yields a valuation, not a Scott-continuous one. This was originally recorded as a gap separate from the question of what the completion contains. They are the same question, and the relation inverts the earlier reading:

If R is a dcpo and μ is Scott-continuous, the metric completion is R itself.

Proof. For a chain x₀ ⊑ x₁ ⊑ ⋯, directedness gives ⊔xₙ ∈ R; continuity gives μ(⊔xₙ) = sup μ(xₙ); μ real-valued makes that finite. So the chain is forward-Cauchy and its limit already lies in R. ∎

Continuity is therefore not machinery needed to make the completion work — it is the condition under which the completion adds nothing. The geometries where valuation genuinely determines new ideal objects are exactly those where R fails to be directed-complete, or μ fails to be Scott-continuous.

Theorem 2 — Scott-continuity implies trivial completion

Completion here is by forward-Cauchy sequences with Yoneda limits (Smyth; Bonsangue–van Breugel–Rutten), the standard notion for quasi-metric domains — not Lawvere's Cauchy-bimodule completion, which is a different object.

Hypotheses. (H1) R directed-complete. (H2) μ Scott-continuous, μ(⊔D) = sup μ(D) for directed D. (H3) μ real-valued.

Under H1–H3, every forward-Cauchy sequence has a Yoneda limit in R; the completion contributes no new ideal points.

Lemma. A forward-Cauchy sequence is eventually a chain. Take ε = 1: some N has d(xₙ,xₘ) < 1 < ∞ for m ≥ n ≥ N, and d is ∞ off the order, so xₙ ⊑ xₘ. ∎

Hence WLOG x₀ ⊑ x₁ ⊑ ⋯, and forward-Cauchy ⟺ sup μ(xₙ) < ∞.

Proof. Let y := ⊔_{n≥N} xₙ — the sup of the tail, not of the whole sequence, since terms before N need not be comparable. Limits depend only on tails. It exists by H1; μ(y) = sup μ(xₙ) by H2, finite by H3.

Case z ⊒ y. Then z ⊒ xₙ for all n, so d(xₙ,z) = μ(z) − μ(xₙ) → μ(z) − μ(y) = d(y,z).

Case z ⊉ y. d(y,z) = ∞. If z ⊒ xₙ for all n then z bounds the chain and z ⊒ ⊔xₙ = y, contradiction; so some x_N ⋢ z, and for n ≥ N, z ⊒ xₙ would give z ⊒ x_N. So d(xₙ,z) = ∞ eventually, and the limit is ∞ = d(y,z). ∎

Nets are identical: the tail of a forward-Cauchy net is directed and increasing.

The case split is exhaustive: z ⊑ y with z ≠ y falls under case 2, since y ⋢ z gives d(y,z) = ∞ and z cannot bound the tail without equalling y.

The completion notion is load-bearing, not a footnote

Under Lawvere's Cauchy-bimodule completion this theorem is vacuous. Lawvere- Cauchy requires convergence in both directions, and d(xₘ,xₙ) = ∞ whenever m > n on a strictly increasing chain. No strictly increasing chain is bi-Cauchy, so that completion is trivial regardless of H1–H3 and the theorem asserts nothing.

The result lives only in the forward-Cauchy/Yoneda setting. This is a hypothesis of the whole programme, not a detail of one proof.

Verification — counterexamples at each hypothesis

¬H1. R = finite subsets of ℕ under ⊆, μ(S) = Σ_{n∈S} 2⁻ⁿ. Real-valued, faithful, continuous where sups exist. The chain {1} ⊂ {1,2} ⊂ ⋯ is forward-Cauchy with μ → 1, but a Yoneda limit needs μ(y) = 1, i.e. y = ℕ ∉ R. Nontrivial completion.

¬H2. R = x₀ ⊏ x₁ ⊏ ⋯ ⊏ ⊤, directed-complete. μ(xₙ) = 1 − 2⁻ⁿ, μ(⊤) = 5: monotone, faithful, finite, discontinuous with defect 4. For z = ⊤, lim d(xₙ,⊤) = 4, so a Yoneda limit needs μ(y) = 1 — no such element. Nontrivial completion, and the gap sits exactly at the defect.

¬H3 differs in kind. With μ(y) = ∞ the expression μ(z) − μ(y) is ∞ − ∞ and d is undefined. H3 is a well-definedness condition on d, not a substantive hypothesis about R, and belongs in the setup rather than the hypothesis list.

Where each hypothesis is load-bearing

H2 is what makes the limit land in R. Without it monotonicity still gives μ(⊔xₙ) ≥ sup μ(xₙ), but strictly. Then

d(⊔xₙ, z) = μ(z) − μ(⊔xₙ) < μ(z) − sup μ(xₙ) = limₙ d(xₙ, z)

so ⊔xₙ is not the Yoneda limit: the sequence converges to an ideal point at value sup μ(xₙ), and ⊔xₙ lies strictly beyond it. A continuity defect of size μ(⊔xₙ) − sup μ(xₙ) is exactly a gap in the completion.

H1 supplies the candidate limit; H3 keeps the subtraction form defined.

Corollary — the classification criterion

A nontrivial completion requires the failure of H1, H2 or H3.

Necessary, not sufficient: a continuity defect creates a gap only if no element of R already occupies the value sup μ(xₙ). The classification therefore splits:

Trivial — H1 ∧ H2 ∧ H3.
No directed-completeness — no candidate limit exists.
No Scott-continuity — a candidate exists but overshoots. Nontrivial iff the defect is unoccupied. Carries the quantitative invariant μ(⊔D) − sup μ(D), the natural coordinate for nontrivial geometries.
No finiteness — only the sum form of d survives. Differs in kind: this makes d undefined rather than making the conclusion fail, so it is a well-definedness condition belonging in the setup. The substantive taxonomy has three cases, not four.

The defect is not the classification coordinate

An earlier form of this section called μ(⊔D) − sup μ(D) "the natural coordinate for classifying nontrivial completion geometries." That is wrong, and the counterexample is immediate.

Take R = x₀ ⊏ x₁ ⊏ ⋯ ⊏ ⊤ with μ(xₙ) = 1 − 2⁻ⁿ, and two valuations differing only in μ(⊤) = 5 versus μ(⊤) = 100. Defects 4 and 99. Both make the chain forward-Cauchy, neither admits a Yoneda limit in R, and both completions add a single point at value 1. Identical convergence behaviour, defects differing 25-fold.

So the defect classifies completions up to isometry; convergence-equivalence is strictly coarser. Under the equivalence actually being classified, the invariant is binary per chain — whether the defect vanishes — not its size.

This is better for tractability, not worse.

The invariant is not novel, and the literature bounds it

μ(⊔D) − sup μ(D) is the failure of continuity from below, classical in two guises:

On chains, it is the jump of a monotone function at a limit point. By Froda's theorem a monotone function has at most countably many jumps.
Measure-theoretically, only in the special case where R is a ring of sets and μ is finitely additive, the gap is the failure of σ-additivity, detected by the purely finitely additive part of the Yosida–Hewitt decomposition (1952). This connection was previously overstated here. μ is in general a monotone function on an arbitrary poset and need not be additive at all, so Yosida–Hewitt does not apply to the general case. What survives generally is only the classical jump.

Corollary, free from Froda: the completion adds at most countably many ideal points per chain. Case 3 of the taxonomy may therefore reduce to a decomposition theorem that already exists.

No-go, correctly scoped

An earlier form of this claim was invalid and is recorded here because the error is instructive: it inferred no symmetry ⟹ no uniqueness, which does not follow. Symmetry is one route to uniqueness; coherence conditions and extremal principles are others. The refuting instance was supplied in the same breath as the claim — subdivision-additivity constrains weights with no symmetry invoked.

No-go (scoped). Provenance blocks symmetry-derived uniqueness. Under the provenance axiom, evidence atoms are pairwise distinguishable, the automorphism group of the evidence structure is trivial, and no invariance-based argument can constrain the weights.

Nothing follows about non-symmetry routes.

Partial positive result. If atoms are distinguishable only by type and exchangeable within type, invariance under block permutations forces wₑ constant on each block. The freedom is then a vector in ℝ^{|T|}_{>0} — one parameter per evidence type — collapsing to a single scale when |T| = 1.

Candidate routes to uniqueness

Route	Mechanism	Status
Symmetry	invariance under an automorphism group	closed by the scoped no-go
Coherence	additivity under evidence subdivision, wₑ = w_{e₁} + w_{e₂}	open; the most reachable
Extremality	surprisal weighting wₑ = −log pₑ, making d the information gained	open; converts the choice into a prior

Subdivision-additivity is the direct analogue of Chentsov's setting, where Markov morphisms are refinements of a sample space. By the Petz precedent, expect a family rather than a point if the evidence structure is non-commutative in the relevant sense — which provenance ordering plausibly makes it.

Program

Complete the representation theorem — close the two technical points above. Mostly bookkeeping.
Prove the scoped no-go — three lines once correctly stated.
Classify minimal additional principles — partitioned by source of uniqueness (symmetry / coherence / extremality), with the first branch known empty. Attack coherence first.
Construct a frame in which Chentsov, Petz and Lawvere are special cases. Reclassified from compare: no such frame is established, and building it is the work. Depends on (3).

What is settled

The refinement order together with a monotone injective evidence embedding determines the order, the Scott topology, and the existence of a faithful quasi-metric — induced, not postulated.

It does not determine the metric topology or the completion. An earlier form of this section said "choosing weights is choosing units". That is too weak, and the counterexample is immediate: for a chain adding one atom per step, uniform weights give d(xₙ,xₘ) = (m−n)w, which is not forward-Cauchy, while decaying weights wₖ = 2⁻ᵏ give d(xₙ,xₘ) < 2⁻ⁿ, which is. The valuation decides whether infinite refinement chains converge — that is, whether the completion contains ideal limit points.

The freedom therefore decomposes:

Component	Effect
global scale wₑ ↦ λwₑ	pure units — preserves Cauchy-ness, completion, all ratios
relative weights across atoms	structural — fixes the metric topology and the completion

Under the one-parameter-per-evidence-type result, exactly one of the |T| parameters is a unit choice; the remaining |T|−1 are structural.

Consequence for the classification program: convergence is a discriminating property between valuation principles. Two principles may agree on scale and still disagree on whether "the fully refined state" exists as an object. Any classification should record it as an axis.

The invariant is coarser than the weighting. A chain converges iff sup_n μ(xₙ) < ∞, so what survives is the partition of infinite chains into convergent and divergent — an ideal-like structure on chains, not a point in ℝ^{|T|}. Many weightings induce one completion, which is good news for tractability: there may be few classes where there are many weightings.

The axiom supplying provenance is still the same axiom removing the symmetry a canonical unit would require — that trade is visible in the axioms. But the residue it leaves is larger than a unit.

Referee findings

Verdict: no new mathematics. Recorded so no later reader mistakes assembly for discovery.

Statement	Status
Theorem 1, (1)⟺(2)	known — Richter–Peleg–Herden, transferred verbatim
Theorem 1, (1)⟺(3)	correct; novelty undetermined. A prior claim that this is "likely known" via Waszkiewicz was withdrawn — it was pattern-matching on subject area, not identification of a theorem
"Eventually a chain" lemma	correct; folklore
Theorem 2	proof valid; novelty UNDETERMINED. See below
Uniqueness (chain additivity + locality)	correct; essentially "a finitely additive set function is determined by its atoms"
Defect over-separation	correction of an error this programme introduced; not a theorem
Provenance destroys symmetry-uniqueness	correct remark about a modelling choice; not mathematics

Corrected here: the Yosida–Hewitt connection was overstated — see above.

The one open item with a plausible claim to novelty is the classification of completion-equivalence classes, if it does not reduce to existing characterizations of Yoneda-completeness. Establishing whether it does is the first thing to do. If it reduces, the programme closes as a survey.

What the programme did produce, and what is worth keeping: the hypotheses are separated by kind, each is witnessed by a counterexample, the completion notion is named rather than equivocated, and the negative results — no canonical scale under provenance, defect over-separates, invariant is classical — are correct. Those are removals rather than additions, and removals were the point.

Withdrawn: the claim that Theorem 2 is known

An earlier referee note stated Theorem 2 is "likely a corollary" of Bonsangue–van Breugel–Rutten (1998), Smyth (1987), or Künzi–Schellekens. That claim is withdrawn. It was reached by pattern-matching on paper titles and subject areas, not by identifying any theorem at the required granularity. No specific result was located, and none could be verified from within the session that asserted it.

Asserting a literature location without being able to name the theorem is a guess in citation form — the same failure this document was written to catch, committed while refereeing.

Revised status: correctness established, novelty undetermined.

A specific reason the expectation may fail

The quasi-metric here is ∞-valued off the order. Much of the quasi-metric domain literature works with everywhere-finite quasi-metrics, which induce richer topologies. Lawvere's generalized metric spaces admit ∞, so the setting is formally in scope — but a general Yoneda-completeness theorem may be stated for the finite case and never specialized here.

The consequence is specific: forward-Cauchy sequences collapse to exactly the μ-bounded chains, a very restrictive class. A general theorem would not automatically be phrased in terms making this case visible, even if it formally covers it. So every ingredient may be classical while this specialization is unwritten.

What would settle it

A characterization of Yoneda-completeness for ∞-valued generalized metric spaces induced by a monotone real function on a poset.
Any statement of the form "a dcpo with a Scott-continuous valuation is Yoneda-complete in the induced quasi-metric."
Treatment of the formal-ball or partial-metric construction for valuations that are monotone but not required continuous — the discontinuous case is where the content lies.

If (2) exists in any form, this is an application note. If only (1) and (3) exist and only in the finite-valued setting, the specialization may be genuinely unwritten.

The kernel of the passage — two corrections and a conjecture

Correction: the completion does NOT forget the defect

An earlier note said the completion "necessarily forgets" μ(⊔D) − sup μ(D). False. Computing inside the completion rather than about it:

d(y*, ⊤) = μ*(⊤) − μ*(y*) = 5 − 1 = 4    (defect for μ₁)
d(y*, ⊤) = 100 − 1        = 99           (defect for μ₂)

The defect is exactly the distance from the ideal point to the old join, and survives intact. The two completions are not isomorphic as quasi-metric spaces — only as sets, and only under convergence-equivalence.

What forgets the defect is the coarser equivalence proposed for classification, not the functor. The object and the equivalence relation placed on it were conflated.

Correction: the passage has four arrows, not three

(R, E)  →  (R, μ)  →  (R, d_μ)  →  Y(R, d_μ)

Provenance is lost at arrow 1, since μ depends on E only through a measure. It is already absent before the metric appears; attributing its loss to the metric passage is a misattribution.

What each arrow loses

Arrow 2 loses almost nothing. The order is recoverable — x ⊑ y ⟺ d(x,y) < ∞ — and μ is recoverable up to one additive constant per order-component; with a bottom, μ(x) = d(⊥,x) exactly. The kernel is precisely the additive constants.

Arrow 3 is a reflection. Y is left adjoint to the inclusion of Yoneda-complete spaces, so two spaces have isomorphic completions iff each is dense in a common complete space. This is standard category theory and no new mathematics is available there.

Reconstruction given the embedding R ↪ Y is immediate: recover d_μ|R, hence the order, hence μ up to constants. Without the embedding R is not intrinsically recoverable — true of every completion, not special here.

Conjecture — the structural characterization

Inserting y* resolves the discontinuity: the chain's join in the completion is y* itself, and μ*(y*) = 1 = sup μ*(xₙ). Continuity holds where it failed.

Conjecture. Y(R, d_μ) is the free Scott-continuous-valuation completion of (R, μ) — left adjoint to the inclusion of (dcpo, continuous valuation) into (poset, monotone valuation). Completion inserts exactly the points needed to make μ continuous, and records each former defect as the distance from the inserted point to the old join.

Structural rather than numerical; explains why the defect survives; checkable.

Novelty: undetermined. This requires the same literature reduction as Theorem 2, and is not guessed at here.

Reconstruction — representation, intrinsicity, sufficiency

(1) What Y represents

From d alone: the refinement order as {(y,z) : d(y,z) < ∞}, and the valuation up to one additive constant per component, μ*(y) = d(⊥,y) where a bottom exists. Y determines (Y, ⊑, μ*) — the same kind of object on a larger carrier.

The specialization order is discrete here. d(y,z) = 0 means y ⊑ z and μ(y) = μ(z), which faithfulness forces to y = z. The refinement order is the finiteness order, a different relation. Any package built on specialization recovers nothing.

(2) R is not intrinsically recoverable — proof

Let R₁ = {x₀ ⊏ x₁ ⊏ ⋯ ⊏ ⊤} with μ(xₙ) = 1 − 2⁻ⁿ, μ(⊤) = 5. Then Y(R₁) = R₁ ∪ {y*} =: R₂. Taking R₂ as the starting object with μ*, it is Yoneda-complete, so Y(R₂) = R₂.

Y(R₁) = Y(R₂) = R₂. Two non-isomorphic valuation objects — one complete, one not — with identical completions. Nothing in Y distinguishes them. ∎

(3) Candidates, evaluated

Candidate	Verdict
Specialization order	insufficient — discrete, per (1)
Scott topology	insufficient — intrinsic to Y, does not select R
Valuation	insufficient — recovered up to constants, does not select R
Defect geometry	insufficient — visible, cannot distinguish inserted from original
Evidence atoms	insufficient — ideal points carry evidence too, as unions along chains
Subdivision structure	insufficient — no mechanism connects it to selection
Distinguished dense subset	sufficient, but it is the embedding renamed
Compactness	sufficient and intrinsic

Sufficient Reconstruction Theorem (conditional). If R = K(Y(R,d_μ)) — the compact elements of the completion — then (R,μ) is recoverable from Y alone, up to additive constants: R = K(Y), μ = μ*|_R.

Compactness is intrinsic: k is compact iff k ⊑ ⊔D implies k ⊑ d for some d ∈ D. No embedding is required to state it.

The hypothesis is load-bearing. In the pair above, K(R₂) = R₁ ≠ R₂, so compactness recovers R₁ regardless of which object one started from. It is a canonical choice, correct exactly when R = K(Y) — i.e. when Y is algebraic with basis R.

This is classical territory: algebraic domains are determined by their compact bases. The sufficient structure is algebraicity, and it is known. Novelty here would lie only in the correspondence, if the correspondence is itself unwritten — the same undetermined literature question as Theorem 2, and not guessed at.

Selection, not reconstruction — corrected statement and scope

The represent/select distinction is sound: compactness is the only candidate that is a predicate on points rather than a structure on the whole, which is why it can partition Y and the others cannot. Scott topology, refinement order, valuation and defect geometry all represent; only compactness selects.

Correction 1 — the circular hypothesis

A proposed form read: "If Y is algebraic and R = K(Y), then …". R is the object being recovered; it cannot appear in the hypotheses and the conclusion. Stated intrinsically:

Selection Theorem (intrinsic form). Let Y be an algebraic Yoneda-complete valuation object. Then (K(Y), μ*|_{K(Y)}) is a valuation object whose Yoneda completion is Y, and it is the unique such preimage consisting of compact elements.

Recovery of a particular R is then a corollary conditional on R = K(Y) — a fact about R, checkable only when R is in hand, and belonging in the corollary.

Correction 2 — an unverified step

Y(K(Y)) = Y is not automatic. Yoneda completion adds points at limiting values; ideal completion adds points at limiting ideals. They coincide only if distinct ideals give distinct Yoneda limits — plausible under faithfulness, since a Yoneda limit is fixed by d(y,z) for all z rather than by μ(y) alone, but unproved. This is the content of the theorem.

Correction 3 — algebraicity excludes a natural class

Counterexample. R = ℚ ∩ [0,1] with μ = id, so d(p,q) = q − p and Y = [0,1]. For x > 0 the directed set [0,x) has supremum x with x ⋢ d for every d < x, so K(Y) = {0} and Y(K(Y)) = {0} ≠ Y.

The theorem fails completely for every densely-ordered refinement system. Algebraicity is a scope restriction, not a regularity condition.

The recovery — algebraicity is the discreteness of recording

Take R = finite subsets of 𝓔 under ⊆, μ = weighted count. A finite S ⊑ ⊔D means S ⊆ ⋃D; each element lies in some member, so directedness gives S ⊆ d for a single d. Every finite-evidence state is compact; infinite ones are not. Hence K(Y) = R exactly.

The Selection Theorem applies precisely when evidence is recorded in discrete atoms and each state carries finitely many.

This pairs with the Representation Theorem's corollary:

	Hypothesis on evidence	Consequence
Representation	countable	a faithful valuation exists
Selection	discrete atoms, finite per state	K(Y) = R; selection recovers the original

Dense refinement — evidence subdividable without limit — satisfies the first and violates the second. The boundary falls out of the counterexample rather than being imposed.

Classification of selectors — initiality, not uniqueness

Uniqueness fails immediately

P(Y) = Y is an intrinsic selector. Y is dense in itself, Y(Y) = Y since Y is complete, and the identity is isomorphism-invariant. It is not compactness: in the ℚ example id(Y) = [0,1] while K(Y) = {0}.

Nor is it isolated — K(Y) ∪ Max(Y) is intrinsic and dense, as is K(Y) joined with any intrinsically-definable set of ideal points. The class of intrinsic selectors is large, and no non-optimisational strengthening obviously excludes the identity.

The lemma that survives

Lemma. Every dense B ⊆ Y contains K(Y).

Proof. Let k ∈ K(Y). B dense makes k the Yoneda limit of a forward-Cauchy sequence (bₙ) ⊆ B; by the eventually-a-chain lemma the tail is a chain, and by the case analysis of Theorem 2 its Yoneda limit is its supremum, so ⊔bₙ = k. Compactness gives k ⊑ bₙ for some n, and bₙ ⊑ k, hence bₙ = k ∈ B. ∎

The theorem

Selector Initiality. For any Yoneda-complete valuation object Y, K(Y) is contained in every dense subset. Hence K is initial in the poset of dense subsets under inclusion, and every intrinsic selector P admits a canonical inclusion K(Y) ↪ P(Y).

K(Y) is itself a selector iff Y is algebraic.

Compactness is not the unique selector; it is the least one. Every sufficient intrinsic selector factors through it — by containment, not equivalence.

The second clause unifies this with the scope result: K(Y) is always the minimum candidate, and is itself dense precisely when Y is algebraic. In the ℚ counterexample K(Y) = {0} lies inside every dense subset while being dense in none — minimum without being sufficient.

Definitional caveat. Under the way-below reading of "basis" rather than "dense subset", id is a selector only for continuous Y and K only for algebraic Y. Uniqueness fails under both readings; only the size of the counterexample class changes.

Reconstruction outside algebraicity — a negative theorem and the structure that replaces it

The fiber always has two intrinsic elements

For Yoneda-complete Y, the fiber {B ⊆ Y : Y(B) = Y} ordered by inclusion has an intrinsic maximum — Y itself, since Y is dense in itself — and an intrinsic infimum, K(Y), by the initiality lemma. The infimum is attained iff Y is algebraic.

Trivial reconstruction is therefore always available; the algebraic case supplies a proper one. The question is what lies between.

Nothing between them is canonical — and this is a theorem

For Y = [0,1] with μ = id, the fiber contains ℚ∩[0,1], the dyadics, the algebraics, uncountably many others. None is distinguished by the order or the metric. This is the standard non-canonicity of bases in continuous domain theory, and is why the field works with abstract bases up to equivalence.

No additional intrinsic structure can select a canonical proper basis outside algebraicity, because the object being selected does not exist.

The search for a better selector terminates negatively.

The structure that does exist is not a subset

The canonical intrinsic object for continuous Y is the way-below relation

x ≪ y  ⟺  for every directed D with y ⊑ ⊔D, some d ∈ D has x ⊑ d

which is intrinsic, order-definable, and determines Y as its round-ideal completion. The abstract-basis framework isolates it precisely because no canonical basis exists.

Compactness is the special case

k ∈ K(Y)  ⟺  k ≪ k

Compactness is reflexivity of ≪. The two results unify:

	Structure	Availability
General	≪ on Y	always intrinsic, for continuous Y
Algebraic	K(Y) = {y : y ≪ y}	the reflexive part; dense iff algebraic

Compactness could never have been the final answer — it is the fragment of ≪ that happens to be a subset. Outside algebraicity the reflexive part is too small ({0} for [0,1]) and the whole relation must be carried.

What this gives and does not give

Gives: (Y, ≪) is a complete intrinsic invariant, recovers Y as its round-ideal completion, and specialises to compactness exactly when ≪ is reflexive on a dense set.

Does not give: recovery of a particular R. That is impossible without extra data, and by the non-canonicity above it is a theorem about bases, not a deficiency of the metric layer. Recovering ℚ from ℝ is the same request.

So the problem "intrinsic structure sufficient to reconstruct the original object without algebraicity" has no solution, for structural reasons. What replaces it is a complete intrinsic invariant under which the original is determined up to the equivalence identifying all bases — the correct sense of "reconstructed" once bases are accepted as non-canonical.

Novelty: undetermined, as with Theorem 2 and the reflection conjecture. Not guessed at.

Closing: the impossibility is informational, not strategic

Correction — ≪ is not additional structure

x ≪ y is defined by quantifying over directed subsets of Y and their suprema — purely from the order — and the order is {(y,z) : d(y,z) < ∞}, purely from d. So (Y, ≪) and Y are the same object; ≪ is a definitional expansion, not extra data.

Therefore "every intrinsic reconstruction factors through (Y, ≪)" reduces to "…factors through Y", which holds of every function of Y by definition. The universality statement is vacuous.

The previous section presented ≪ as "the structure that replaces the basis". That overstated it: ≪ names a relation already present and supplies nothing Y did not have.

The theorem that actually closes the question

Theorem. Let F be any isomorphism-invariant construction on Yoneda-complete valuation objects — of any shape: subset, relation, category, functor. Then F(Y(R₁)) = F(Y(R₂)), because the arguments are the same object. Hence no F recovers both.

Witness. R₁ = {x₀ ⊏ x₁ ⊏ ⋯ ⊏ ⊤} with μ(xₙ) = 1 − 2⁻ⁿ, μ(⊤) = 5; R₂ := Y(R₁), which is Yoneda-complete so Y(R₂) = R₂ = Y(R₁). R₁ and R₂ are non-isomorphic — R₂ has an element at value 1, R₁ does not. ∎

No intrinsic reconstruction of R exists, and bases have nothing to do with it. The completion functor is not injective. Whether a candidate reconstruction is a subset of Y, a relation on Y, or an object of an unrelated category is irrelevant: all are functions of Y, and Y does not determine R.

The non-canonicity-of-bases argument given earlier is a special case of this, restricted unnecessarily to subset-valued strategies. Sound, but weaker than needed.

The only escape is not one

Reconstruction "up to an equivalence" succeeds iff the equivalence identifies R₁ with R₂ — iff it identifies every object with its own completion. That is exactly "same completion", under which reconstruction is trivially successful and recovers nothing.

What survives

Selector Initiality is unaffected, being a statement about Y's internal structure rather than about recovering R: K(Y) lies in every dense subset, is initial among them, and is itself dense iff Y is algebraic.

The programme closes on non-injectivity of the completion functor — stronger and simpler than non-canonicity of bases, and admitting no strategic workaround.

The (R₁,R₂) pair is not a theorem

Y is a reflection. For any reflection L with unit η_X : X → LX:

if η_X is not an isomorphism then X ≇ LX;
but LX lies in the reflective subcategory, so L(LX) ≅ LX;
hence L(X) ≅ L(LX) while X ≇ LX.

Non-faithfulness on isomorphism classes holds for every reflection whose unit is not always invertible. No hypotheses about valuations, orders or metrics enter.

The (R₁,R₂) pair is that construction with a chain substituted for X. The same example, older and better known: ℚ and ℝ have the same metric completion. Likewise any poset and its ideal completion, any group and its profinite completion.

So the non-faithfulness is neither a known theorem of valuation objects nor a new theorem of this programme. It is a special case of the defining property of a non-trivial reflection — elementary category theory, verifiable by construction, requiring no citation.

The impossibility corollary — F(Y(R₁)) = F(Y(R₂)) because the arguments are equal — is "a non-injective map has no inverse", phrased with more symbols.

Recorded failure mode

Two sections above, this document already states:

"Arrow 3 is a reflection … two spaces have isomorphic completions iff each is dense in a common complete space. This is standard category theory and no new mathematics is available there."

That is the non-faithfulness. It was written, classified as standard, and then two turns later a special case of it was constructed and presented as the witness closing the programme.

This is the fourth contribution in this line of work to dissolve on inspection, and the failure mode is specific: each time, the "new" result was a special case of something already recorded in the same document. Distinct from the literature-guessing failure — this one needs no external check, only reading the existing notes.

Status

Result	Status
Representation Theorem	Richter–Peleg–Herden, transferred
Theorem 2	correct; novelty undetermined
Selector Initiality	correct; elementary
Non-faithfulness of Y	generic property of reflections
Impossibility corollary	restatement of non-injectivity

No novel mathematical result. The only item whose novelty is genuinely undetermined remains Theorem 2 and the reflection conjecture, pending a literature reduction not performed here.

What is not reflection theory — Theorem 2 strengthened

Q1: Theorem 2 is not a manifestation of the abstract theory

Reflection theory says L(X) ≅ X iff X lies in the reflective subcategory — a tautology that says nothing about which concrete objects are members. That information is never available abstractly. Theorem 2 supplies exactly it.

But it was stated too weakly, and the converse was never attempted.

Counterexample to the converse as originally stated. R = ℕ with μ(n) = n. Forward-Cauchy requires μ-differences → 0, and μ is integer-valued, so such sequences are eventually constant and have limits. (R, d_μ) is Yoneda-complete but not a dcpo — ℕ is directed with no supremum. Full directed-completeness is unnecessary because unbounded directed sets are not Cauchy.

Theorem 2′. (R, d_μ) is Yoneda-complete iff every μ-bounded directed subset of R has a supremum at which μ is continuous.

(⟸) A forward-Cauchy sequence is eventually a chain with sup μ < ∞, hence μ-bounded directed; the hypothesis gives its supremum with μ(⊔D) = sup μ(D), and the Theorem 2 case analysis makes it the Yoneda limit.

(⟹) Let D be μ-bounded directed. Given ε > 0 pick d₀ ∈ D with μ(d₀) > sup μ(D) − ε; any d ⊒ d₀ in D has μ(d) − μ(d₀) < ε, so D is forward-Cauchy as a net. Completeness supplies a Yoneda limit, identified by the case analysis as ⊔D with μ(⊔D) = sup μ(D). ∎

H1 and H2 fuse into one condition, and the result becomes a characterization rather than a sufficient condition.

Q2: the Representation Theorem is imported, not derived

It cannot be obtained from enrichment or domain theory plus reflection, because it concerns neither. (1)⟺(2) is Richter–Peleg–Herden — when a poset admits a strictly isotone map into ℝ — from order theory and mathematical economics. (1)⟺(3) is a translation once (1) is available. The programme consumes that theorem rather than producing it.

Q3: the programme is therefore not purely synthesis

Result	Status
Representation Theorem	imported from order theory
Non-faithfulness, impossibility corollary	generic reflection theory
Selector Initiality	elementary, internal to Y
Theorem 2′	characterization of the reflective subcategory in concrete terms

Theorem 2′ is where novelty must lie if it lies anywhere. Its status is unchanged — undetermined, pending a literature reduction not performed here — but it is now the right kind of statement to be new, and sharper than when the question was asked.

Theorem 2′ — full proof

Setup. (R,⊑) a preorder; μ : R → [0,∞) monotone; d(x,y) = μ(y) − μ(x) if x ⊑ y, else ∞.

A net (xᵢ) is forward-Cauchy if ∀ε>0 ∃i₀ ∀j≥i≥i₀ : d(xᵢ,xⱼ) < ε. A point y is a Yoneda limit if d(y,z) = limᵢ d(xᵢ,z) for every z. R is Yoneda-complete if every forward-Cauchy net has a Yoneda limit.

Theorem 2′. (R,d_μ) is Yoneda-complete iff every μ-bounded directed subset of R has a supremum at which μ is continuous.

Lemma 0 — antisymmetry is derived, not assumed

If μ is faithful, ⊑ is antisymmetric. Suppose x ⊑ y ⊑ x with x ≠ y; monotonicity gives μ(x) ≤ μ(y) ≤ μ(x), so μ(x) = μ(y), contradicting faithfulness. ∎

Lemma 1 — eventual monotonicity

Take ε = 1. Some i₀ has d(xᵢ,xⱼ) < 1 < ∞ for j ≥ i ≥ i₀; d finite forces xᵢ ⊑ xⱼ. ∎

Lemma 2 — the tail is directed

For i,j ≥ i₀ pick k ≥ i,j in the directed index set; Lemma 1 gives xᵢ ⊑ x_k and xⱼ ⊑ x_k. ∎

Lemma 3 — μ-boundedness

With ε = 1 and j ≥ i₀: μ(xⱼ) − μ(x_{i₀}) < 1, so sup μ(T) ≤ μ(x_{i₀}) + 1. ∎

Lemmas 1–3: every forward-Cauchy net's tail is a μ-bounded directed subset.

Lemma 4 — the limit in the definition exists

Write aᵢ = d(xᵢ,z). Triangle gives aᵢ ≤ d(xᵢ,xⱼ) + aⱼ for j ≥ i, so aᵢ − aⱼ ≤ d(xᵢ,xⱼ). Given ε choose i₀ with d(xᵢ,xⱼ) < ε for j ≥ i ≥ i₀; then aⱼ > aᵢ − ε, so liminf a ≥ aᵢ − ε for every i ≥ i₀, hence limsup a ≤ liminf a + ε. ε arbitrary, so the limit exists. (If aᵢ = ∞ then aⱼ = ∞ for all j ≥ i, and the limit is ∞.) ∎

Without Lemma 4 the definition of Yoneda limit is not well-posed.

(⟸) Hypothesis ⟹ Yoneda-complete

Let (xᵢ) be forward-Cauchy with tail T; by 1–3 it is μ-bounded directed, so the hypothesis gives y = ⊔T with μ(y) = sup μ(T).

Case y ⊑ z. For i ≥ i₀, xᵢ ⊑ y ⊑ z, so d(xᵢ,z) = μ(z) − μ(xᵢ) → μ(z) − μ(y) = d(y,z).

Case y ⋢ z. d(y,z) = ∞. If d(xᵢ,z) < ∞ cofinally then xᵢ ⊑ z cofinally; for any j ≥ i₀ choose cofinal i ≥ j with xᵢ ⊑ z, so xⱼ ⊑ xᵢ ⊑ z. Then z bounds T and y ⊑ z — contradiction. So d(xᵢ,z) = ∞ eventually and the limit is ∞. ∎

(⟹) Yoneda-complete ⟹ hypothesis

Let D be μ-bounded directed, s = sup μ(D) < ∞, indexed by itself.

D is forward-Cauchy. Given ε pick d₀ ∈ D with μ(d₀) > s − ε; for d' ⊒ d ⊒ d₀, d(d,d') = μ(d') − μ(d) ≤ s − μ(d₀) < ε.

Completeness is used exactly once, to supply a Yoneda limit y. The rest is the Yoneda condition at two test points.

y is an upper bound. At z = y: 0 = d(y,y) = lim_d d(d,y), so d ⊑ y cofinally; for arbitrary d' pick d ⊒ d' with d ⊑ y, giving d' ⊑ y.

μ(y) = s. d(d,y) = μ(y) − μ(d) → 0, so μ(y) = lim μ(d) = s.

y is least. For any upper bound u, d(d,u) = μ(u) − μ(d) → μ(u) − μ(y). The Yoneda condition at z = u gives d(y,u) = μ(u) − μ(y) < ∞, and finiteness of d means y ⊑ u. ∎

Exactly what is used

Property	Where	Needed
μ monotone	d ≥ 0, well-definedness	yes
μ real-valued	subtraction defined; Lemma 3	yes
μ faithful	Lemma 0 only — antisymmetry, hence unique suprema	only there
d = ∞ off the order	Lemma 1 and both ⋢ arguments	yes, essentially
Antisymmetry	—	derived (Lemma 0)
Continuity, algebraicity, sobriety, T₀	nowhere	not needed

The proof never appeals to a topology; it is order-theoretic and arithmetic throughout.

Precision not previously stated. The converse requires net-completeness, not sequential. D may be uncountably directed and need not admit a cofinal sequence. Under a sequences-only definition of Yoneda-completeness, (⟹) is unproved and may fail.

Verification of Theorem 2′ — four technical checks

1. Triangle inequality, all cases. Split on x ⊑ y, then y ⊑ z.

A: x ⊑ y and y ⊑ z. Transitivity gives x ⊑ z; both sides finite; d(x,z) = μ(z) − μ(x) = (μ(y) − μ(x)) + (μ(z) − μ(y)). Equality.
B: x ⊑ y, y ⋢ z. d(y,z) = ∞, so RHS = ∞.
C: x ⋢ y. d(x,y) = ∞, so RHS = ∞.

No case yields ∞ − ∞: in A both terms are finite by real-valuedness and non-negative by monotonicity. Equality holds exactly in case A, which is why chains give equality and everything else is slack.

2. d(d,y) → 0 gives EVENTUAL comparability, not merely cofinal. lim_d d(d,y) = 0 unpacks to ∀ε>0 ∃d₀ ∀d ⊒ d₀ : d(d,y) < ε. With ε = 1, for all d ⊒ d₀ we get d(d,y) < ∞, and finiteness is comparability, so d ⊑ y. For arbitrary d' ∈ D directedness gives d ⊒ d',d₀, whence d' ⊑ d ⊑ y. The earlier phrasing "cofinally" was weaker than the limit delivers and required a superfluous step.

3. Uniqueness of suprema is needed for NOTATION ONLY. (⟸) picks a supremum y of T at which μ is continuous, using only μ(y) = sup μ(T) and the least-upper-bound property. (⟹) constructs a y, proves it is an upper bound, and proves it lies below every upper bound — exhibiting a supremum. Neither direction uses uniqueness. Lemma 0 is required only so that ⊔D denotes. Stated existentially, the theorem needs no antisymmetry.

Consequence: faithfulness is not a hypothesis of Theorem 2′. Without it d may satisfy d(x,y) = 0 for x ≠ y, which Lawvere quasi-metrics permit. Lemmas 1, 3, 4 and both directions survive verbatim — none consults faithfulness. It matters only for d to be T₀-separating, which is never invoked.

Minimal hypotheses: μ monotone and real-valued.

4. D as index category. D carries the restriction of ⊑, a directed preorder by assumption, hence a legitimate net index; the net is the inclusion D ↪ R, d ↦ d. Forward-Cauchy for it reads ∀ε ∃d₀ ∀d' ⊒ d ⊒ d₀ : d(d,d') < ε, which is what the proof establishes.

Caveat upstream of both open questions: the definitions are unverified

The definitions used throughout were stated from memory and have not been checked against the literature:

forward-Cauchy: ∀ε ∃i₀ ∀j≥i≥i₀ : d(xᵢ,xⱼ) < ε
Yoneda limit: d(y,z) = limᵢ d(xᵢ,z) for all z

The literature carries variants — some formulate Yoneda limits via presheaves or bimodules rather than pointwise limits, some use liminf — and for ∞-valued spaces these are not obviously interchangeable. Lemma 4 exists only because the pointwise version requires the limit to exist, which a presheaf formulation would not.

If the definition of Yoneda limit is non-standard, Theorem 2′ is about a different object and everything downstream inherits that.

So the open questions are ordered, not independent:

Are the definitions standard? — literature, gates the rest
Given (1), is the proof correct? — proof-checking
Given (1) and (2), is the characterization new? — literature

Status: correctness UNVERIFIED, novelty UNDETERMINED, definitions UNCHECKED. Three verification passes found a real defect each time — the tail-supremum error, the vacuous universality claim, the superfluous faithfulness hypothesis. That is evidence the statement has been stressed, not evidence it is correct. All checking to date has been self-checking, which in this investigation has a documented poor record.

Endpoint — the candidate equivalence

The programme's output is not a candidate theorem — that phrasing centres a proof artifact. It is a candidate equivalence whose status is unresolved:

For a monotone, real-valued valuation μ on a preorder, with d(x,y) = μ(y) − μ(x) when x ⊑ y and ∞ otherwise:

net-Yoneda completeness of d ⟺ every μ-bounded directed subset has a supremum at which μ is continuous.

Three questions remain, properly ordered, each gating the next:

Definition validation. Do "forward-Cauchy net" and "Yoneda limit" as used here match the standard literature, or what is the precise translation?
Equivalence verification. Under those definitions, does the equivalence hold? A referee pass, not self-checking.
Literature reduction. Does the equivalence already exist, follow immediately from known results, or is it absent?

(1) is by far the cheapest and gates the other two: if the definitions are non-standard, (2) and (3) are not yet well-posed.

What the programme produced independent of novelty

It began with many competing conjectures — truth density, ontological fidelity, nine proposed coordinates, continuous rendering fidelity, a hierarchy of languages. It ends with one precise candidate equivalence, minimal hypotheses, explicit proof obligations.

That reduction is genuine progress even if the equivalence proves to be known, because it converted a research direction into a falsifiable statement. The mechanism was expensive — most of the narrowing came from claims being made and refuted rather than from foresight — and the durable artifact is therefore the record of what was eliminated and why, which is what makes the surviving question sharp.

Theory closed here. Next step is external verification, in the order above.