[FIX] CONTROL-A written: the first kernel-sound control document

61/61 units sound. A=0, N=0, D=43, Q=5, X=13. All five quotations resolve
verbatim against ~/CLAUDE.md, the single axiom source.

The document derives, from five constitutional clauses, a conclusion the
constitution nowhere states: that detection and correction are priced
differently, and that a practice pricing them alike suppresses a required act by
appeal to a prohibition that does not reach it. 'detect' appears nowhere in
CLAUDE.md — checked before writing, so the derivation is not inert.

The kernel's own ordering rule shaped the form. §2's D may rest only on what is
established EARLIER, so the clauses must precede the derivation and the title may
not state the conclusion. The constraint produced the right document.

TWO JOINTS WERE REMOVED IN DRAFT 3 RATHER THAN DEFENDED, and that is the most
load-bearing work in the file:

 · Draft 2 concluded that detecting drift in THIS FILE is required, resting on
   the review-cadence clause, whose trigger is a 'stated review date'. CLAUDE.md
   states a revision CADENCE ('revised yearly'), which is not the same thing. The
   gap had been bridged by interpretation wearing the clothes of derivation. The
   conclusion never needed the application to this file, so the claim was narrowed
   to what the clauses carry.
 · Draft 2 routed the first horn of the reductio through Constraint 4 ('the
   system must report its own limits'). 'Limit' is undefined in the axiom set, so
   any obligation drawn from it is interpretation. The ESCALATE taxonomy row
   governs the same case exactly, in the source's own words, and replaced it.

Finding them was the point of writing it as if it mattered. §6.2's falsifier is
'a document passes every check and a competent adversarial reader still finds an
undemonstrated load-bearing claim' — better found by the author first.

Also fixed, two tool defects of the same class this programme exists to catch:
 · reduce.py still printed 'kernel v1.0' after v1.1 was frozen — every run record
   carried a provenance line naming the wrong governing document.
 · §3.1 did not enforce v1.1's A-prohibition. A control tagged A now FAILS: needing
   an assumption means the claim is not derivable from §1, and naming it is exactly
   what v1.1 forbids. Reduction runs may show A; a control may not.

NOT a soundness verdict. §4's six judgement residues are untouched by any check,
and §6.2 requires an adversarial read by a party that is neither the document's
author nor an author of the kernel. That read has not happened.
This commit is contained in:
David F Glidden
2026-08-02 18:20:37 +02:00
parent 3d0d9d6f27
commit a7b833caa6
4 changed files with 247 additions and 2 deletions
+19 -2
View File
@@ -56,7 +56,13 @@ from pathlib import Path
# excluding it would quietly shrink the quarantine in the author's favour.
SPLITTER_VERSION = "1.2.0"
KERNEL_SHA256 = "67c9b870491db7444e98b680c7c80dcd99de376dda09b3e1758b27b1229ab045"
# The kernel this tool enforces. It was left at v1.0's hash after v1.1 was
# frozen, so every run record printed a provenance line that named the wrong
# governing document — the tool asserting a fact about itself that the substrate
# contradicted, which is the class this whole programme exists to catch.
KERNEL_VERSION = "1.1"
KERNEL_SHA256 = "d4b48db23612b30ff66e26b6235065a3c2f3c9be19d750dafc97e80a1329974d"
KERNEL_FILE = "CONTROL-KERNEL-v1.1.md"
TAGS = {"D", "Q", "A", "N", "X"}
@@ -437,6 +443,17 @@ def cmd_check(doc: Path, tags_path: Path) -> None:
if stray:
failures.append(f"§3.1 STRAY TAGS on non-assertive spans: {stray[:12]}")
# v1.1 §2a/§3.1 — `A` is a diagnostic, not a tag. A control document that
# carries one is not kernel-sound: needing an assumption means the claim is
# not derivable from §1, and naming it is precisely what v1.1 forbids.
# Reduction runs may legitimately show `A`; a CONTROL may not.
a_tagged = sorted(i for i, (t, _) in tags.items() if t == "A")
if a_tagged:
failures.append(
f"§2a A-FREE VIOLATION: {len(a_tagged)} unit(s) tagged A: {a_tagged[:12]}. "
"A control document must derive or quote the claim, or §1 must widen."
)
# §3.2 — every Q resolves verbatim in a declared axiom source.
available = {k: p for k, p in AXIOM_SOURCES.items() if p.is_file()}
missing = sorted(set(AXIOM_SOURCES) - set(available))
@@ -462,7 +479,7 @@ def cmd_check(doc: Path, tags_path: Path) -> None:
reasons[r] = reasons.get(r, 0) + 1
print(f"document {doc.name}")
print(f"kernel v1.0 sha256 {KERNEL_SHA256[:16]}…")
print(f"kernel v{KERNEL_VERSION} ({KERNEL_FILE}) sha256 {KERNEL_SHA256[:16]}…")
print(f"splitter v{SPLITTER_VERSION}")
print(f"tagged {len(tags)} of {len(taggable_idx)} assertive units")
print("counts " + " ".join(f"{t}={counts[t]}" for t in sorted(TAGS)))