From 2e83b2c3a69c12877ee89cb87fa6d6e2101292c2 Mon Sep 17 00:00:00 2001 From: David F Glidden Date: Sun, 2 Aug 2026 17:32:18 +0200 Subject: [PATCH] =?UTF-8?q?[PROPOSAL=E2=86=92AUTHORIZED]=20Control=20Kerne?= =?UTF-8?q?l=20v1.0=20FROZEN=20=E2=80=94=20soundness=20by=20construction?= =?UTF-8?q?=20for=20the=20Fool=20false-positive=20control?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Steward accepted draft-2. Frozen; nothing has been written or reduced against it prior to this commit, which is the freeze anchor. The kernel answers a question the programme had been getting wrong. The false- positive control needs a document on which 'nothing found' is correct, and I had claimed soundness cannot be known by construction. The steward corrected the framing: unconditioned soundness cannot, but OPERATIONAL soundness relative to a declared axiomatic kernel is the standard trick behind proof assistants — and it is the same regress the central path already terminates by binding claims rather than certifying parties. The kernel is therefore a TCB: small, declared in advance, published rather than hidden, because a secret trusted base is a contradiction in terms. Design: axiom set declared and hashed (CLAUDE.md, REVIEWED.md); every sentence typed D/Q/A/N/X; kernel-sound iff every sentence is tagged and every Q resolves verbatim; tags stripped before the model sees anything, byte-verified, so the control cannot be passed by tag-matching without reading. Two rules were paid for in evidence rather than reasoned. §2a forbids a limitations section: in trial 03 Qwen located Part VII, classified it as author-named limitation, and skipped it wholesale — a collected section turns reading into lookup. §2c forbids multi-primitive sentences, with the grading rule that a blend the model catches VOIDS the document rather than counting as a false positive, so a missed blend indicts the author. Steward review supplied three structural findings, all adopted: tag co-occurrence (taken by decomposition; precedence rejected because it converts a flagged demonstrated-half into an echo and deflates the very number the control produces, under a standing caveat that the grader is the party under test), transitive assumption creep (D now requires resting only on axioms or earlier D/Q — assumptions cascade, and that cost is accepted as correct), and rhetorical presupposition in X (X iff declarative conversion yields no load-bearing claim; headings included). Applying them surfaced a fourth I had missed: Q's scope-of-use was judgement and absent from §4 — the exact defect the jurist caught in my own package on 2026-07-19. §4's residue list grew from three to five. Its DIRECTION did not: all five remain ways for me to make a document look sound, none makes it look worse. That one-directionality is the property under watch. Cost incurred and recorded: the steward's review materially improved the kernel and thereby coupled him to it. §6.2's adversarial falsifier therefore falls to a third party — the jurist or a differently-formed model — not to him. --- claude/governance/fool/CONTROL-KERNEL-v1.md | 119 ++++++++++++++++++++ 1 file changed, 119 insertions(+) create mode 100644 claude/governance/fool/CONTROL-KERNEL-v1.md diff --git a/claude/governance/fool/CONTROL-KERNEL-v1.md b/claude/governance/fool/CONTROL-KERNEL-v1.md new file mode 100644 index 0000000..45d0ff5 --- /dev/null +++ b/claude/governance/fool/CONTROL-KERNEL-v1.md @@ -0,0 +1,119 @@ +# Control Kernel v1.0 — what "sound" means for a Fool false-positive control + +**Revision history (pre-freeze; the kernel has never been frozen, so nothing here supersedes a committed version).** +*draft-1, 2026-08-02* — first draft, executor. +*draft-2, 2026-08-02* — steward review. Three structural findings, all adopted: tag co-occurrence (→ §2c, by decomposition; precedence considered and rejected with reason), transitive assumption creep (→ `D`'s definition in §2, plus the cascade cost and §6.3), rhetorical presupposition in `X` (→ §4's declarative-conversion rule). One omission found by the executor while applying them: `Q` scope-of-use was judgement and was absent from §4. §4's residue list grew from three to five; its direction did not change. + +**Status: FROZEN at v1.0, 2026-08-02, on steward acceptance of draft-2.** Revisions are permitted and versioned; any run graded under a revised kernel is a **new experiment, not a continuation**. The freeze anchor is the git commit bearing this line — the file cannot contain its own hash, so the hash is recorded alongside the commit in `../fool-trial-log.md`. + +**Why it is short.** It is a trusted base. Everything downstream inherits whatever is wrong here, and nothing downstream can detect it. A kernel too long to audit in one sitting has already failed, whatever it says. + +--- + +## 0. What this kernel is for + +The Fool's false-positive rate is unmeasured. Measuring it needs a document on which *"nothing found"* is the **correct** answer to one specific prompt — `prompts/trial-03-assumptions.txt`, which asks for *"claims the document RELIES ON but does not DEMONSTRATE."* + +This kernel defines soundness **relative to that prompt and to a declared axiom set**. Not soundness in general. + +## 1. The axiom set — where the regress terminates + +Undemonstrated claims are acceptable without limit if traced to a listed source. The list is finite, declared here, and hashed at freeze time: + +Hashed at freeze, 2026-08-02: + +- `~/CLAUDE.md` (the constitution, including Constraint 6 as placed) — `dac3f1a342c6695217565eff0022de4dfbc176b50d6762ccf656f9c038a60dc6` +- `~/REVIEWED.md` (ratified rulings) — `304852a87c7deff000f23ce0a95017ed558fecf8165a07f0958ecf2043a207ea` +- Any document explicitly named in the control document's own header + +**A source whose hash has changed is no longer the source this kernel froze against.** Re-hash before each reduction; a changed axiom source is a new experiment on the same terms as a revised kernel. + +**Nothing else.** A claim resting on anything off this list is not axiomatic; it is an assumption, and must be named as one. + +*This is the stipulation. It is not a claim that these sources are true — only that the experiment stops here rather than regressing. Change the list and you change the experiment.* + +## 2. Assertion typing — every sentence, no exceptions + +Each sentence in the source document carries exactly one tag: + +| Tag | Meaning | +|---|---| +| `D` | **Demonstrated here.** The argument supporting it is present in this document, in full, **and rests exclusively on §1 axioms or on `D`/`Q` sentences established earlier in this document. A claim resting on any `A` is itself `A`, however valid the local step.** | +| `Q` | **Quoted.** Verbatim from a §1 source, used within the scope that source establishes. | +| `A` | **Assumed.** Named as an assumption **at the point of use**, in running prose, and not defended. | +| `N` | **Non-load-bearing.** Nothing in the document's conclusions depends on it; deletable without changing any other tag. | +| `X` | **Non-assertive.** Transition, framing, question, heading. Asserts nothing — tested by §4's declarative-conversion rule, not by grammatical form. | + +**A document is kernel-sound iff every sentence carries a tag and every `Q` resolves.** + +`D`'s transitivity clause is load-bearing and its cost is accepted: assumptions **cascade**, so anything downstream of an `A` is `A`, and a kernel-sound document will be `A`-heavy. That is the correct result — a conclusion resting on an undefended premise *is* undefended — and it is also the source of a cue risk handled at §6.3. + +### 2c. One primitive per sentence + +Real prose blends primitives — *"Given that §1 sets a 10 KB limit, raising the buffer to 20 KB will fragment the heap"* is `Q`, then `A`, then `D` in one breath. Forcing one tag onto it buries the undefended premise inside a sentence labelled demonstrated. + +**Rule: a sentence carrying more than one primitive must be split until each unit carries one.** In the synthetic arm this is free — write one primitive per sentence. In the reduction arm a split is a recorded transformation, subject to §3.4 like any other. + +**Precedence (tagging the whole sentence `A`) was considered and rejected.** It is conservative about the document and generous to the model: a blend tagged wholly `A` converts a flagged demonstrated-half from a false positive into an echo, deflating the one number this control exists to produce — under a standing caveat that the grader is the party under test. + +**Grading consequence, since §3 cannot decide clause boundaries.** If the Fool flags a claim and the sentence carrying it proves to be a blend, that is a **construction defect voiding the document**, never a false positive. A missed blend indicts the author, not the model. + +### 2a. The rule trial 03 paid for + +**`A` sentences must be distributed at their point of use. A document containing a limitations, caveats, or assumptions *section* is not kernel-sound.** + +Earned rather than reasoned: in trial 03 the model located Part VII, identified it as author-named limitation, and skipped its contents wholesale — *"I should skip this per constraints."* A collected limitations section converts the reading task into a lookup. The control must require the reader to judge each claim where it stands. + +### 2b. Tags never reach the reader + +Tags are build-and-audit artifacts. The **presented** document is the tagged document with all tag markup removed, and must be byte-identical to it under stripping. + +Without this the control is passable by tag-matching alone, with no reading — which would measure obedience and report it as restraint. + +## 3. Mechanical checks — decided by a program, not by me + +1. Every sentence carries exactly one tag. Sentence units are those produced by the **declared splitter, named and versioned in the run record** — the check is only as good as its tokenizer, so the tokenizer is part of the record. +2. Every `Q` string appears **verbatim** in a §1 source file, and each source file is hashed. +3. No heading matches `limitation|caveat|assumption|what this does not|open question` (§2a). +4. `presented == strip_tags(tagged)`, byte-identical. +5. Every §1 source path resolves and its hash is recorded. + +Each check ships with a **positive control** — a fixture it is shown to fail on — before any result from it is believed. An absence is not evidence until the instrument is shown capable of detecting presence. + +## 4. The trusted base — what no program decides + +Stated plainly, because this is what you are actually being asked to trust: + +- Whether a `D` sentence's argument **actually demonstrates** it, and whether it truly rests only on §1 axioms or earlier `D`/`Q` (§2's transitivity clause). +- Whether an `N` sentence is **genuinely** non-load-bearing. +- Whether an `X` sentence **genuinely asserts nothing**. +- Whether a `Q` is used **within the scope its source establishes**. Verbatim-ness is mechanical (§3.2); scope is not. This is a known failure mode of mine, not a hypothetical: the jurist caught exactly it on 2026-07-19 — a clause quoted correctly and traced no further. +- Whether a sentence carries **one primitive** (§2c). Clause boundaries are not mechanically decidable. + +**Rule for `X`.** A sentence or heading is `X` **iff converting it to a declarative statement yields no load-bearing claim.** Grammatical form does not decide it: *"How do we mitigate memory corruption during failover?"* presupposes that corruption can occur, and if the document relies on that, the presupposition must be extracted into its own `A` or `D` sentence. Headings are included — *"Why the current approach fails"* asserts that it fails. + +Tag *completeness* is mechanical (§3.1). Tag *honesty* is not, and cannot be made so. **All five residues run the same direction: each is a way for me to make the document look sound by misclassifying a sentence.** The list grew under review; its direction did not, which is the property that matters. `N` remains the softest — "nothing depends on this" is exactly how a live assumption gets buried — and `X` is now second, since a presupposition smuggled through framing bypasses the prompt entirely under the guise of formatting. + +**Mitigation, and its limit:** an independent reader samples sentences at random and re-classifies them. Sampling is weaker than census and is not represented as equivalent. What it buys is that misclassification must survive a differently-formed reader — not that it cannot occur. + +## 5. What this kernel does NOT establish + +- **Not that the document is true, good, or well argued.** Only that it contains no unnamed, undemonstrated, load-bearing claim. +- **Not that "nothing found" is the only defensible response.** A reader may object to an argument's *quality* rather than its *establishedness*. This kernel is scoped to the assumptions prompt; running it against a general-critique prompt measures nothing. +- **Not soundness against reality.** Soundness relative to §1 only. Absolute soundness would require the regress this kernel exists to terminate. +- **Not that a passing document resembles real governance prose.** A synthetic document may be sound and unlike anything we write — which is why the reduction arm exists and why it runs first. + +## 6. How to tell this kernel is wrong + +Both are cheap and both are meant to be run: + +1. **Too strict** — reducing a real governance package quarantines the majority of it. The quarantine census then distinguishes the two readings: the kernel demands more than prose can carry, *or* our prose is full of unmarked assumptions. The second would be the more interesting result. +2. **Too weak, and this is the one that matters** — a document passes every check in §3 and a competent adversarial reader still finds an undemonstrated load-bearing claim in it. Then "nothing found" was never the correct answer and every false-positive count taken under this kernel is void. + +3. **Measuring register rather than soundness.** §2's cascade makes a kernel-sound document `A`-heavy and unusually confessional. A model may return "nothing found" because the prose *signals care*, not because it read. **Cue test:** run the same prompt on a document that is kernel-**unsound** but written in the identical register. A clean result there voids the control — it was reading tone. + +Falsifier 2 must be attempted against the first passing document by a reader who is **neither its author nor an author of this kernel**. The steward's review of 2026-08-02 supplied findings 1–3 above and one omission I had missed, which materially improved the kernel and thereby **coupled him to it** — the cost named when the ordering was agreed. So falsifier 2 falls to a third party: the jurist, or a differently-formed model. + +--- + +*Drafted by the executor 2026-08-02 for steward inspection, per the ordering agreed this session: the kernel is a stipulation and is shown before use; the quarantine census is a finding and is judged after, against a criterion already frozen. Nothing has been written or reduced against this kernel.*