From f6efe516a1a8e4c4deaccbf440c78771f0d4b715 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sun, 30 Aug 2026 04:48:03 +0700 Subject: [PATCH] skill(ci-gates) 342: the proof was provable because the model was wrong 341 declined to hand-write Lean models, reasoning that a faithful model might make its theorem false and that a red build would then be indistinguishable from a transcription error. An audit of the existing models found the same thing from the other side. `specs/tri/utils/args.t27` declares `fn parse(allocator: std.mem.Allocator)` -- one parameter. Its model declares three, the dotted path split on its dots, and the env was given `("Std", [("value", .u32)])` to match: a name in zero of the 650 specs and exactly once in the Lean file. The fabrication is load-bearing. `Ty.isLowerableFuel` rejects a `.struct` with empty fields, so a faithful model is not lowerable and the theorem is false. `icarus-lowerable` on that spec prints `not_lowerable`, and `t27c parse` shows one parameter with the dotted path intact, so the split is not mirroring the AST either. 16 models carry the split. Fifteen assert `= false`, where a wrong model changes nothing. The one asserting `= true` is the one where the fabrication decides the answer. An unfaithful model is worse than an empty one: the 114 empty models announce themselves, and this one lists four correctly-named functions in spec order and looks checked. Refs #2893 --- .claude/skills/ci-gates/SKILL.md | 44 +++++++++++++++++++ docs/now/2026-08-30-provable-because-wrong.md | 12 +++++ 2 files changed, 56 insertions(+) create mode 100644 docs/now/2026-08-30-provable-because-wrong.md diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index 5225698b73..ab56bc966e 100644 --- a/.claude/skills/ci-gates/SKILL.md +++ b/.claude/skills/ci-gates/SKILL.md @@ -8589,3 +8589,47 @@ exist yet — in the one medium where the claim is a PROOF. The honest substitute is the count, and saying plainly which of the two things you did. + +## 342. The proof was provable because the model was wrong + +§341 declined to hand-write four Lean models, on the reasoning that a +FAITHFUL model might make its theorem false, and that a red build would +then be indistinguishable from a transcription error. + +An audit of the existing models found the same thing from the other +side, and it is sharper than the argument. + +`specs/tri/utils/args.t27` declares `fn parse(allocator: std.mem.Allocator)` +— one parameter. Its Lean model declares three: + + params := [("allocator", (.struct "Std")), ("mem", (.u32)), + ("Allocator", (.u32))] + +The dotted type path was split on its dots. And the env was given a +struct to match: `("Std", [("value", .u32)])` — a name that appears in +**zero of the 650 specs** and exactly **once** in the Lean file. + +That fabrication is what makes the theorem provable. `Ty.isLowerableFuel` +rejects a `.struct` whose fields are empty, so a faithful model — one +parameter of the undeclared type `std.mem.Allocator` — is not lowerable +and the theorem is `false`. The compiler agrees: `icarus-lowerable` on +that spec prints `not_lowerable`. + +The same split appears in 16 models. Fifteen assert `= false`, where a +wrong model changes nothing. **The one that asserts `= true` is the one +where the fabrication decides the answer.** + +Two things follow. + +**An unfaithful model is worse than an empty one.** The 114 empty models +announce themselves: `functions := []` says the theorem is about +nothing. This one lists four functions, all named correctly, in spec +order, with tests populated. It looks checked. One signature is invented +and that signature is load-bearing. + +**And the risk §341 declined to take was real, in the direction it +predicted.** Not "I might transcribe it wrong and CI would tell me" — +somebody already transcribed one wrong, and no instrument has told +anybody, because nothing builds these proofs. A medium where a wrong +artefact is indistinguishable from a right one, and no build ever runs, +does not become safe by adding more artefacts to it. diff --git a/docs/now/2026-08-30-provable-because-wrong.md b/docs/now/2026-08-30-provable-because-wrong.md new file mode 100644 index 0000000000..bf36a6856f --- /dev/null +++ b/docs/now/2026-08-30-provable-because-wrong.md @@ -0,0 +1,12 @@ +# NOW -- The proof was provable because the model was wrong (2026-08-30) + +## An audit found from the other side what 341 declined to risk (Refs #2893) + +- `specs/tri/utils/args.t27` declares `fn parse(allocator: std.mem.Allocator)` -- ONE parameter +- its Lean model declares THREE: the dotted type path was split on its dots into `allocator`, `mem`, `Allocator` +- and the env was given `("Std", [("value", .u32)])` to match -- a name in ZERO of the 650 specs and exactly once in the Lean file +- that fabrication is load-bearing: `Ty.isLowerableFuel` rejects a `.struct` with empty fields, so a faithful model makes the theorem FALSE +- the compiler agrees with the faithful reading: `icarus-lowerable` prints `not_lowerable` +- and it is not mirroring the AST: `t27c parse` shows one parameter with the dotted path intact +- the same split is in 16 models; 15 assert `= false` where a wrong model changes nothing, and the ONE asserting `= true` is where it decides the answer +- an unfaithful model is worse than an empty one: the 114 empty ones announce themselves, this one lists four correctly-named functions in spec order and looks checked