# Relations and statement shapes The ledger as a graph. `related_result_ids` in [`registry.yaml`](../../registry.yaml) records *that* two results are related; `relations` records *how*, and `result_shape` records what kind of statement a row makes at all. Coverage: **31 typed edges** across **19 rows**, and **31 rows** carry a shape, out of **144** results (77 of which record untyped adjacency). This is a pilot scoped to the self-knowledge cluster. An untyped row is not a claim that the row has no relations — it is a claim that nobody has decided them. ## Why shape matters A point impossibility rules out one corner of a design space and says little about the rest. A characterization says what *is* achievable as well as what is not. Recording which is which makes the difference visible without reading each row's prose. | Shape | Meaning | Rows | |---|---|---| | `ACHIEVABILITY` | a construction attaining something | LAND-CL-001, LAND-SOV-CAPABILITY-001 | | `BOUND` | an inequality, so it degrades rather than switching off | LAND-ACCUM-001 | | `CHARACTERIZATION` | necessary and sufficient — says what *is* achievable as well as what is not | LAND-ACCESS-ORDER-001, LAND-AMBIG-001, LAND-AUDIT-REGISTRY-001, LAND-EVAL-BLINDSPOT-001, LAND-GOODHART-REGTARGET-001, LAND-JOINTOBS-001, LAND-KNOW-001, LAND-KNOW-UNIFORM-001, LAND-SELFMEAS-003, LAND-SELFREF-001, LAND-SOV-ASSESSMENT-001, LAND-VERIF-FULLACCESS-001 | | `INFRASTRUCTURE` | definitions and transfer lemmas, no standalone claim | LAND-CAUSAL-DECISION-001, LAND-CAUSAL-DECISIONNET-001, LAND-CAUSAL-PEARLCBN-001, LAND-CAUSAL-STRUCTURAL-001, LAND-KNOW-DEVICE-001, LAND-SOV-DEONTIC-001, LAND-SOV-INSTITUTION-001, LAND-SOV-STABILITY-001, LAND-TEMPORAL-001 | | `POINT_IMPOSSIBILITY` | rules out one extreme configuration | BY-044, LAND-AUDIT-LAG-001, LAND-CAUSAL-COLLISION-001, LAND-CRMDP-KNOW-001, LAND-INCIDENT-COUNT-001, LAND-SELFMEAS-001, LAND-SELFMEAS-002 | ## Edge kinds | Kind | Meaning | |---|---| | `BOUNDARY_PARTNER` | one rules something out, the other constructs something nearby; the note states the model delta | | `BUILDS_ON` | the source row's Lean proofs call the target row's declarations | | `INSTANTIATES` | the source row is the target's general statement at a specific model | | `REFINES` | the source row gives a sharper form of the target's statement | ## Typed edges | From | Kind | To | Why | |---|---|---|---| | LAND-ACCUM-001 | `BUILDS_ON` | LAND-AMBIG-001 — Finite fibre ambiguity and the counting obstruction | The window bounds are stated and proved in terms of ambiguity and its fibre image. | | LAND-ACCUM-001 | `BUILDS_ON` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | not_knowable_pairTarget_of_not_knowable is Knowable.mono against the projection. | | LAND-ACCUM-001 | `BUILDS_ON` | LAND-TEMPORAL-001 — Time-indexed knowability, contemporaneous collisions, and delayed knowledge | ambiguity_le_of_evidenceMonotone consumes Temporal.EvidenceMonotone: cumulative evidence makes the earlier observation a post-processing of the later one, so ambiguity_le_of_comp applies along time. | | LAND-AMBIG-001 | `BUILDS_ON` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | knowable_iff_ambiguity_le_one is proved through knowable_iff_no_collision. | | LAND-AMBIG-001 | `REFINES` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | Replaces the qualitative iff with a count of the answers a single observation leaves open, at the cost of finiteness and decidable equality. Knowability becomes ambiguity at most one. | | LAND-CAUSAL-DECISION-001 | `BUILDS_ON` | LAND-CAUSAL-COLLISION-001 — Margins do not imply behavioral identifiability | Consumes the causal Model, derived Skeleton utility gap, margin class, and masked transform layer. | | LAND-CAUSAL-KNOW-001 | `BUILDS_ON` | LAND-CAUSAL-DECISION-001 — Causal decision policies, regret, and identified-set radius | Reads Skeleton, Model.Delta-mask and BehaviorEq from the decision layer and restates them; proves nothing further about causal models. | | LAND-CAUSAL-KNOW-001 | `BUILDS_ON` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | Every theorem here is a kernel law at the causal observation: the collision law, the classical witness extraction, and Knowable.mono. The module proves no factorization law of its own. | | LAND-CAUSAL-STRUCTURAL-001 | `BOUNDARY_PARTNER` | LAND-CAUSAL-DECISION-001 — Causal decision policies, regret, and identified-set radius | Parallel, not layered. Causal.Decision is the unmediated Assumption-1 projection and this is the mediated diagram; no declaration connects them. That missing map no longer holds Richens and Everitt Section 2.2 back: those rows closed on 2026-09-20 through Causal.DecisionNetwork instead (expectedUtility_eq_value, regret_eq_value_regret), and are graded Same in section 6 of the coverage audit. | | LAND-CL-001 | `BOUNDARY_PARTNER` | LAND-SELFMEAS-001 — Self-measurement failure for an embedded observation | Not a formal duality: the two do not share a model. This row is the generic whole-state specialization of the knowability kernel, not Breuer's theorem, which is LAND-SELFMEAS-002: an abstract restriction map from global states to apparatus states, with no dynamics, no messages and no algorithm; Chandy-Lamport's is a message-passing distributed system with channels, markers and a recording procedure. What the pair brackets is contemporaneity. The impossibility is about distinguishing the state one is in *now*; the construction recovers a consistent global state by giving up exactly that, recording a cut rather than an instant. | | LAND-COMP-KNOW-001 | `BUILDS_ON` | LAND-ANGLUIN-001 — Port-labelled anonymous networks, views, and automorphisms | The no-collision premise is runFor_eq_of_view_eq verbatim. This row restates that theorem and proves nothing further about networks. | | LAND-COMP-KNOW-001 | `BUILDS_ON` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | knowable_runFor is the kernel's knowable_iff_no_collision applied to the depth-n view and the state after n rounds; the module proves no factorization law of its own. | | LAND-COMP-TRACE-001 | `BUILDS_ON` | LAND-ANGLUIN-001 — Port-labelled anonymous networks, views, and automorphisms | not_electsLeader_of_fixedPointFree is no_unique_leader_of_fixedPointFree transported across the producer; nothing further about networks is proved. | | LAND-COMP-TRACE-001 | `BUILDS_ON` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | not_knowable_node_of_fixedPointFree is the kernel's not_knowable_of_invariant_transform at the node-observation map, with the automorphism as the transform; the module proves no factorization law of its own. | | LAND-CRMDP-KNOW-001 | `BUILDS_ON` | BY-039 — Reward corruption unsolvability | Both ingredients are BY-039's module: history_complement supplies the collision and return_add_complement supplies the disagreement. | | LAND-CRMDP-KNOW-001 | `INSTANTIATES` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | Takes the state to be the unknown environment, the observation to be the history a fixed policy receives, and the target to be the true finite-horizon return. | | LAND-HYPER-KNOW-001 | `BUILDS_ON` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | knowable_of_isSafetyPredicate is the kernel's knowable_iff_no_collision applied to the realized-observation map and the safety predicate; the module proves no factorization law of its own. | | LAND-JOINTOBS-001 | `BUILDS_ON` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | Covers and Refines are definitionally the kernel's Knowable and Determines, so Coverage and RepairBoundary discharge their proofs by calling the kernel rather than repeating a factorization argument. | | LAND-KNOW-DEVICE-001 | `BOUNDARY_PARTNER` | BY-024 — Physical limits on inference | Model delta: Knowable asks one decoder to work at every state, while Definition 3 fixes the conclusion function and lets the choice of setup block vary with the probe. The quantifier alternation is why neither implies the other, and why the transports below are conditional rather than an identification. | | LAND-KNOW-DEVICE-001 | `BUILDS_ON` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | Consumes IndistinguishabilityWitness as the object crossing the joint and produces Knowable in the positive direction; neither component of the device's pair suffices alone. | | LAND-PREF-KNOW-001 | `BUILDS_ON` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | not_knowable_reward is the kernel's not_knowable_of_collision applied to op3 and Prod.snd; the module proves no factorization law of its own. Determines.refl and Determines.trans are added to the kernel itself rather than here. | | LAND-SELFMEAS-001 | `INSTANTIATES` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | The whole-state case: the target is the identity, so knowability is injectivity of the observation. | | LAND-SELFMEAS-002 | `BUILDS_ON` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | not_knowable_state_of_properInclusion hands the proper-inclusion pair straight to not_knowable_of_collision. | | LAND-SELFMEAS-003 | `BUILDS_ON` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | knowable_whole_state_iff_injective is knowable_id_iff_injective at the apparatus reading. | | LAND-SELFMEAS-003 | `BUILDS_ON` | LAND-SELFMEAS-002 — Breuer abstract embedded-measurement core | Derives ProperInclusion under product-complement or finite-cardinality hypotheses, then applies the core no-meshing_measures_all theorems. | | LAND-SELFMEAS-003 | `REFINES` | LAND-SELFMEAS-001 — Self-measurement failure for an embedded observation | Composition restates the product remainder obstruction and feeds it into the Breuer measurement model, not only the Knowable skeleton. | | LAND-SELFREF-001 | `BUILDS_ON` | LAND-AMBIG-001 — Finite fibre ambiguity and the counting obstruction | card_rest_le_one_of_selfComplete is proved through card_image_le_of_knowable rather than by a separate cardinality argument. | | LAND-SELFREF-001 | `INSTANTIATES` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | Takes the state to be Model times Rest and the observation to be the first projection, so the observer is a component of what it observes. | | LAND-TEMPORAL-001 | `BOUNDARY_PARTNER` | LAND-CL-001 — Chandy-Lamport distributed snapshot — termination, correctness, stable property detection | Model delta: this row is an arbitrary indexed family of observations over an arbitrary preorder, with no dynamics and no communication; Chandy-Lamport is a concrete message-passing system with an algorithm. The pair brackets contemporaneity, not one model's frontier: DelayedKnowable says the current target can be unreadable while a later reading settles it, and the snapshot algorithm is the motivating instance of that pattern rather than a construction inside this model: nothing here is applied to it, and no theorem connects the two. | | LAND-TEMPORAL-001 | `BUILDS_ON` | LAND-KNOW-001 — Exact knowability: the observation-factorization kernel | knowableFrom_mono is Knowable.mono and not_knowableAt_of_collisionAt is not_knowable_of_collision; no factorization argument is re-proved. | | LAND-VERIF-AGENTBEHAVIOR-001 | `BUILDS_ON` | BY-012 — Rice's theorem | no_behavioral_safety_verifier reduces to the atlas's rice packaging of Mathlib's ComputablePred.rice and reproves nothing. BY-012 is the row for that route; this row is the row for the statement Melo et al. make. | ## Boundary pairs The pairs worth reading together: an impossibility and a nearby construction. These are **not** formal dualities — the two sides rarely share a model, which is why every such edge is required to carry the delta. ### LAND-CAUSAL-STRUCTURAL-001 ↔ LAND-CAUSAL-DECISION-001 - **LAND-CAUSAL-STRUCTURAL-001** (INFRASTRUCTURE) — Structural causal models, causal influence diagrams, and materiality - **LAND-CAUSAL-DECISION-001** (INFRASTRUCTURE) — Causal decision policies, regret, and identified-set radius Parallel, not layered. Causal.Decision is the unmediated Assumption-1 projection and this is the mediated diagram; no declaration connects them. That missing map no longer holds Richens and Everitt Section 2.2 back: those rows closed on 2026-09-20 through Causal.DecisionNetwork instead (expectedUtility_eq_value, regret_eq_value_regret), and are graded Same in section 6 of the coverage audit. ### LAND-CL-001 ↔ LAND-SELFMEAS-001 - **LAND-CL-001** (ACHIEVABILITY) — Chandy-Lamport distributed snapshot — termination, correctness, stable property detection - **LAND-SELFMEAS-001** (POINT_IMPOSSIBILITY) — Self-measurement failure for an embedded observation Not a formal duality: the two do not share a model. This row is the generic whole-state specialization of the knowability kernel, not Breuer's theorem, which is LAND-SELFMEAS-002: an abstract restriction map from global states to apparatus states, with no dynamics, no messages and no algorithm; Chandy-Lamport's is a message-passing distributed system with channels, markers and a recording procedure. What the pair brackets is contemporaneity. The impossibility is about distinguishing the state one is in *now*; the construction recovers a consistent global state by giving up exactly that, recording a cut rather than an instant. ### LAND-KNOW-DEVICE-001 ↔ BY-024 - **LAND-KNOW-DEVICE-001** (INFRASTRUCTURE) — Transports between the knowability kernel and inference devices - **BY-024** (unshaped) — Physical limits on inference Model delta: Knowable asks one decoder to work at every state, while Definition 3 fixes the conclusion function and lets the choice of setup block vary with the probe. The quantifier alternation is why neither implies the other, and why the transports below are conditional rather than an identification. ### LAND-TEMPORAL-001 ↔ LAND-CL-001 - **LAND-TEMPORAL-001** (INFRASTRUCTURE) — Time-indexed knowability, contemporaneous collisions, and delayed knowledge - **LAND-CL-001** (ACHIEVABILITY) — Chandy-Lamport distributed snapshot — termination, correctness, stable property detection Model delta: this row is an arbitrary indexed family of observations over an arbitrary preorder, with no dynamics and no communication; Chandy-Lamport is a concrete message-passing system with an algorithm. The pair brackets contemporaneity, not one model's frontier: DelayedKnowable says the current target can be unreadable while a later reading settles it, and the snapshot algorithm is the motivating instance of that pattern rather than a construction inside this model: nothing here is applied to it, and no theorem connects the two.