Files

T

David F Glidden 2e83b2c3a6 [PROPOSAL→AUTHORIZED] Control Kernel v1.0 FROZEN — soundness by construction for the Fool false-positive control

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.

2026-08-02 17:32:18 +02:00

11 KiB

Raw Blame History

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

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.
Every Q string appears verbatim in a §1 source file, and each source file is hashed.
No heading matches limitation|caveat|assumption|what this does not|open question (§2a).
presented == strip_tags(tagged), byte-identical.
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:

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.
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.
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.

11 KiB Raw Blame History Unescape Escape