docs/closure-verification.md
Closing the graphs, and re-verifying every separation over them
The governing conclusion, recorded first:
No semantic transformation can be verified over an open representation graph.
This is the rendering analogue of the projection ledger's requirement that every information-preserving claim name its observable object. An open graph is not incomplete coverage — it is a verification precondition that has not been satisfied. A separation measured over an open graph is unverifiable in principle, not merely unverified in practice.
Step 1 — closing the remaining graphs
Openness had exactly two causes. They resolved differently.
Animation — CLOSED
link.flow drives a useFrame loop; a single-frame snapshot could not see it.
@react-three/test-renderer exposes advanceFrames, which makes it observable
with no new dependency.
Measured: after advanceFrames(30, 16) a traffic mesh has moved from the origin
to (11, 0.5, 13) — the link endpoint. Now a permanent test.
Html — NOT CLOSABLE with any instrument available
Measured, not assumed:
- Under the test renderer,
Htmlrenders nothing. The jsdombody.innerHTMLis length 0; the label text appears in neither the scene graph nor the DOM. drei'sHtmlportals into a canvas parent the test renderer never creates. - The browser instrument cannot reach it either: the page rendering
WorldSceneis session-gated (getSessioninapp/page.tsx), and authenticating as the operator is outside what I may do.
What would close it, in order of honesty:
- A browser-based instrument driven by the operator, holding a real session — the standing constraint makes session-gated probes the user's action.
- Extracting the label-colour decision into an exported pure function, with the call site verified by parser. This is structural closure, not observational: it proves the function is correct and is called, not that the pixel is right. It should be labelled as the weaker grade, not counted as closure.
Closure has grades, and conflating them would repeat the substitution defect:
| Grade | Meaning |
|---|---|
| Observational | the rendered output is measured |
| Structural | the carrier derives from a tested function whose call site is verified |
| Open | neither |
Correction — the two instruments disagree, and the parser under-counts
The source parser reported status with one carrier (wireframe). Measured
at the render, status has three: position.y, emissiveIntensity,
wireframe.
The parser missed two because they are computed into variables rather than
written as inline attribute expressions referencing .status. The render is
authoritative for carrier counts; the parser is a lower bound.
Every carrier count in semantic-locality.md is therefore a floor, not a
figure. The closure verdicts survive — all three status carriers are in the
scene graph, so it remains closed — but the counts do not.
Corrected closure table
| Fact | Carriers (measured) | Observable | Closure |
|---|---|---|---|
activity |
2 | 2/2 | closed |
status |
3 (was 1) | 3/3 | closed |
flow |
2 | 2/2 (animation now instrumented) | closed |
identity |
≥4 | 3/4 | open — span.style |
health |
≥3 | 2/3 | open — span.style |
blocked |
≥2 | 1/2 | open — span.style |
Three of six closed, up from two. Every remaining open graph has the same
single cause: span.style.
Steps 2 and 3 — re-running every separation over its graph
| Separation | Graph | Verdict |
|---|---|---|
unstaffed vs idle |
status — closed |
VERIFIED |
identity vs alert (emissive) |
identity — open |
remains provisional |
uncertainty (health=unknown → opacity) |
health — open |
remains provisional |
The one that survives
Re-measured over the closed status graph:
steady y=3.20 int=1.5 wf=false
idle y=2.20 int=0.35 wf=false
unstaffed y=2.20 int=0.35 wf=true ← distinguished by wireframe alone
unstaffed and idle share two carriers and are separated by the third. Since
all three are observable, this separation is verified, not provisional — the
first semantic separation in this renderer to reach that standing.
The ones that do not
Both remaining separations touch facts whose graphs are open at span.style.
Their earlier "success" was measured over the instrumented subset only, and the
measurement could not have detected relocation into the uninstrumented carrier —
which is precisely what happened to identity/alert.
They are not reported as failures. They are reported as unverifiable, and that distinction is the point: the evidence does not exist either way.
An unrelated collision, still standing
active and steady differ in 0 slots. This is the collision the
reachability correction flagged: it matters only if status = active ∧ blocked = 0 is reachable, which remains unresolved and is not a closure
question.
Status against the sequence
- Close every representation graph — animation done;
span.styleblocked on an instrument I cannot build. - Re-run separations over closed graphs — done. 1 verified, 2 unverifiable.
- Record which survive — done, above.
- Legend amendments — not yet. Two of three separations remain unverifiable, and the Legend must ratify semantics that survived verification over closed graphs.
The single blocker for steps 1–3 is now one carrier, and closing it requires either an operator-run browser instrument or an explicit decision to accept structural closure as sufficient for that carrier. Both are the user's call, not mine.