From 1cc05d9cce889e4f4d4e306cd59b61382425f432 Mon Sep 17 00:00:00 2001 From: Shay Date: Wed, 27 May 2026 07:52:20 -0700 Subject: [PATCH] =?UTF-8?q?docs:=20schema-defined=20proof=20obligations=20?= =?UTF-8?q?doctrine=20+=20convergence-site=20invariant=20+=20FOLLOWUPS=20?= =?UTF-8?q?=C2=A76=20(#360)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three small surgical anchors capturing the verified architectural insight surfaced during the ADR-0167 wave (no new ADR — the gap claim that prompted this resolved on verification; what remains is a sharper residual question worth memorialising). 1. CLAUDE.md — new "Schema-Defined Proof Obligations" section between Documentation Discipline and Validation Through CLI. Generalises the wrong=0 invariant pattern: schema types that name structural properties are real only when an executing test can meaningfully fail under the violations it is written to catch. Three-step rule for treating a schema as load-bearing. 2. language_packs/compiler.py — ARCHITECTURAL INVARIANT comment on _apply_mounted_primary_domain_resonance naming it as the single convergence-decision site for DEPTH_ROOT/DEPTH_RELATION packs. Anchors the doctrine at the code site so any future modification trips on the reference to the holonomy proof's coverage gap. 3. docs/handoff/ADR-0167-FOLLOWUPS.md §6 — captures the structural-vs- blend convergence isolation question. HolonomyAlignmentCase IS executed today (we verified), but the existing test doesn't distinguish structurally-derived convergence from blend-induced convergence. Ablation test or reframed claim — both acceptable resolutions. Verified before commit: - All 13 architectural references in the Gemini analysis resolve exactly: triliteral 0.30, root 0.40, prefix 0.03/(idx+1), stem 0.24, _INFLECTION_PRIORITY case-near-last, _apply_mounted_primary_domain_resonance with 40% English-prototype blend, HolonomyAlignmentCase defined AND executed - tests/test_alignment_graph.py: 8 passed (no behavioural change) - Documentation discipline (#355) honoured: pure Markdown, no HTML No code behaviour changes. No runtime effect. Drops the larger ADR-0168-PROPOSAL idea — the gap claim that prompted it dissolved under verification. --- CLAUDE.md | 26 ++++++++++++ docs/handoff/ADR-0167-FOLLOWUPS.md | 66 ++++++++++++++++++++++++++++++ language_packs/compiler.py | 19 +++++++++ 3 files changed, 111 insertions(+) diff --git a/CLAUDE.md b/CLAUDE.md index a3f50fa1..83236374 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -236,6 +236,32 @@ Out of scope: Diagrams go inside the doc that needs them. Specs do not become single-file applications. +## Schema-Defined Proof Obligations + +When a schema, type, or struct exists for the sole purpose of naming a +structural property the architecture claims to hold +(``HolonomyAlignmentCase``, ``RoundTripFilter``, the various ``Result`` +discriminants), the obligation is real only when an executing test can +**meaningfully fail** under the violations it is written to catch. + +A test that passes under conditions that bypass the obligation it +nominally proves is decoration, not proof. Before treating a schema +type as a verified property: + +1. Identify the violations the schema is written to catch. +2. Confirm an existing test would fail if exactly one of those + violations were silently introduced (e.g. by mutating a weight, + skipping a step, swapping a fallback). +3. If no such test exists, the obligation is asserted but not proven — + record the gap in a follow-up doc rather than treating the schema + as load-bearing. + +This rule generalises the wrong=0 invariant. ``wrong == 0`` holds +because the admissibility gate, the round-trip filter, and the +multi-branch disagreement check are all wired to fail loudly when +violated. The same discipline applies to every other "this design +guarantees X" claim in the codebase. + ## Validation Through CLI Use CLI lanes instead of ad hoc pytest fragments: diff --git a/docs/handoff/ADR-0167-FOLLOWUPS.md b/docs/handoff/ADR-0167-FOLLOWUPS.md index 3b6e00ce..9e1f3f40 100644 --- a/docs/handoff/ADR-0167-FOLLOWUPS.md +++ b/docs/handoff/ADR-0167-FOLLOWUPS.md @@ -194,6 +194,69 @@ for math). --- +## 6. HolonomyAlignmentCase — structural-vs-blend convergence isolation + +**Scope.** Determine whether the existing +`tests/test_alignment_graph.py::test_holonomy_alignment_case_positive_closer_than_negative` +proves *structurally-derived* cross-language convergence or only proves +*endpoint similarity under the mount-time blend*. + +**Why deferred.** The proof obligation is executed today — the test +asserts that an aligned Logos clause produces nearer holonomies across +English/Hebrew/Greek than a misaligned negative triple. That clears the +schema's nominal claim. But the test does not distinguish two possible +explanations for the convergence: + +1. **Structural.** The Hebrew tri-consonantal root rotors and Greek + case-last orientation rotations produce versors that genuinely + land in the same regions of the manifold because the morphology + operators encode equivalent semantic structure. +2. **Blend-induced.** `_apply_mounted_primary_domain_resonance` + (`language_packs/compiler.py:558`) nudges Hebrew/Greek versors + toward an English prototype at 40% blend, and the test passes + because both packs have been pulled close to the English anchor + regardless of structural derivation. + +If (2) is doing the work, the three-language architecture is a *claim* +that English-anchored geometric averaging produces the right endpoints, +not a *proof* that the depth packs are structurally independent +operators converging coherently with the articulation surface. + +**Where breadcrumbs live.** +- `language_packs/compiler.py::_apply_mounted_primary_domain_resonance` + — the architectural-invariant comment names this gap explicitly and + references this section +- `tests/test_alignment_graph.py:73` — the existing positive-closer- + than-negative assertion +- `language_packs/schema.py::HolonomyAlignmentCase` — the schema type + whose nominal contract is "proves structural divergence with + coherent convergence" + +**Acceptance.** One of: +- **(a) Ablation test.** A test that runs the holonomy proof with + `_apply_mounted_primary_domain_resonance` disabled (or with the + blend factor set to 0.0) and asserts that the positive-closer-than- + negative relation still holds. This would prove (1) and retire the + concern. +- **(b) Reframe the claim.** If the ablation fails, document + explicitly that cross-language convergence depends on the + mount-time blend, and update `HolonomyAlignmentCase`'s contract to + reflect what it actually proves (endpoint similarity under blend, + not structural-derivation equivalence). Honest documentation of a + weaker property beats a stronger claim that the test can't support. + +**Priority.** Low-urgency, high-information. Not blocking any current +capability gate. Worth picking up whenever someone next touches the +language-pack architecture — the comment at the convergence-decision +site is the trip-wire. + +Per CLAUDE.md §"Schema-Defined Proof Obligations" — this is the +prototypical example of a schema-defined obligation that is executed +but where the test may not meaningfully fail under the violation it is +written to catch. + +--- + ## Sequencing recommendation For the operator picking this up next: @@ -208,6 +271,9 @@ For the operator picking this up next: 4. **Defer §4 + §5** until §1 actually ships a second sub-type — they only become load-bearing once a second domain candidate type exists. +5. **Pick up §6 opportunistically** — whoever next modifies + `_apply_mounted_primary_domain_resonance` or the holonomy test owns + the ablation question. No timelines. Order is by leverage, not calendar. diff --git a/language_packs/compiler.py b/language_packs/compiler.py index ba1b9445..ea1dd237 100644 --- a/language_packs/compiler.py +++ b/language_packs/compiler.py @@ -559,6 +559,25 @@ def _apply_mounted_primary_domain_resonance( mounted: VocabManifold, primary_groups: dict[str, list[tuple[str, str]]], ) -> None: + # ARCHITECTURAL INVARIANT — single convergence-decision site. + # + # This function is the one place in the codebase where DEPTH_ROOT and + # DEPTH_RELATION packs (Hebrew, Greek) have their structurally-derived + # versors blended toward an English prototype at mount time. Any + # modification — to the 0.40 blend factor, the prototype-selection + # rule, or the grouping logic — must consider whether the + # ``HolonomyAlignmentCase`` proof in + # ``tests/test_alignment_graph.py::test_holonomy_alignment_case_positive_closer_than_negative`` + # still demonstrates cross-pack structural divergence rather than + # blend-induced convergence. The existing test asserts aligned + # endpoints are closer than misaligned endpoints; it does not yet + # isolate structural derivation (Hebrew/Greek morphology operators) + # from this function's nudge. See ``docs/handoff/ADR-0167-FOLLOWUPS.md`` + # §6 for the open isolation question. + # + # Per CLAUDE.md §"Schema-Defined Proof Obligations": if you weaken + # this site, verify the holonomy test would still fail under the + # weaker condition you allowed. for surfaces in primary_groups.values(): languages = {language for language, _ in surfaces} if len(languages) < 2: