docs: schema-defined proof obligations doctrine + convergence-site invariant + FOLLOWUPS §6 (#360)
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.
This commit is contained in:
parent
97b0ee0e13
commit
1cc05d9cce
3 changed files with 111 additions and 0 deletions
26
CLAUDE.md
26
CLAUDE.md
|
|
@ -236,6 +236,32 @@ Out of scope:
|
||||||
Diagrams go inside the doc that needs them. Specs do not become
|
Diagrams go inside the doc that needs them. Specs do not become
|
||||||
single-file applications.
|
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
|
## Validation Through CLI
|
||||||
|
|
||||||
Use CLI lanes instead of ad hoc pytest fragments:
|
Use CLI lanes instead of ad hoc pytest fragments:
|
||||||
|
|
|
||||||
|
|
@ -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
|
## Sequencing recommendation
|
||||||
|
|
||||||
For the operator picking this up next:
|
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
|
4. **Defer §4 + §5** until §1 actually ships a second sub-type — they
|
||||||
only become load-bearing once a second domain candidate type
|
only become load-bearing once a second domain candidate type
|
||||||
exists.
|
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.
|
No timelines. Order is by leverage, not calendar.
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -559,6 +559,25 @@ def _apply_mounted_primary_domain_resonance(
|
||||||
mounted: VocabManifold,
|
mounted: VocabManifold,
|
||||||
primary_groups: dict[str, list[tuple[str, str]]],
|
primary_groups: dict[str, list[tuple[str, str]]],
|
||||||
) -> None:
|
) -> 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():
|
for surfaces in primary_groups.values():
|
||||||
languages = {language for language, _ in surfaces}
|
languages = {language for language, _ in surfaces}
|
||||||
if len(languages) < 2:
|
if len(languages) < 2:
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue