Surmount miscellaneous specifications

This repository holds small, precise specifications maintained by Surmount. Each numbered document is a standalone technical spec. The zero document is the spec spec: form rules for how the rest are written.

Table of contents

1. What this repository is
2. Current specifications
3. Document rules
4. Versioning and publication
5. RFC 2119 requirement keywords
6. External references (ref/)
7. Validation (Lean and Nix)
   1. Local and CI gate (Nix is primary)
   2. Authoritative checkers
      1. Why Lean vs pure Nix
   3. Run Lean directly
   4. Run via Nix
   5. Systems Lean meaning proofs
   6. beastdb meaning proofs and the number registry
   7. SSSSS meaning proofs
   8. CATE meaning proofs
   9. RSI meaning proofs
   10. CI meaning proofs
   11. Formal Vibefication spec encodings and proofs
   12. Surmount composition proof
   13. Sibling line encodings
8. Development shell and pre-commit
9. Residual
10. Project skill /surmount-specify
11. Project skill /rsi
12. Project skill /lean4
13. License

1. What this repository is

Surmount miscellaneous specifications are short normative documents for interfaces, formats, and design constraints that do not belong in a larger product tree. Specs are pure ASCII markdown, written in American English, versioned with real Semantic Versioning when published, and checked by automated tools packaged through Nix.

Numbered specifications live only in the repository root as files named NNNN_descriptive_name.md (for example 0000_spec.md, 0001_DOGE.md, 0002_Systems_Lean.md, 0003_beastdb.md, 0004_SSSSS.md, 0005_CATE.md, 0006_RSI.md, 0007_CI.md, 0008_Formal_Vibefication.md, 0010_Surmount_Systems.md). They are not nested under a specs/ subdirectory or similar. That flat root layout is the same spirit as the bitcoin/bips repository: numbered proposals at the root. Number 0009 is withdrawn. The file 0009_VOCABULARY.md MUST NOT exist. The word catalog lives in CATE (0005_CATE.md).

The binding rules for form live in 0000_spec.md. This README orients humans and agents; it is not itself a full specification.

2. Current specifications

1. 0000_spec.md - Surmount spec spec (spec 0), version 1.3.0. Defines how specs in this repository are written, named, versioned, cited, and checked. Concise American Technical English (CATE) is specified in 0005_CATE.md. This document keeps a short pointer only and does not restate CATE. Authors SHALL follow 0005_CATE.md when writing numbered specifications. 0000_spec.md is version 1.3.0.
2. 0001_DOGE.md - Digital Octal Graphical Emissive (DOGE) color specification, version 1.0.0. Defines a pure 3 bit RGB palette of eight colors with fixed sRGB values, ECMA-48 SGR mapping, and two quantization methods. Uses RFC 2119 requirement keywords; cites RFC 2119, ECMA-48, and ITU-T T.416 / ISO/IEC 8613-6 under ref/.
3. 0002_Systems_Lean.md - Systems Lean, version 1.0.0. Defines Lean 4 with linear and affine ownership and Quantitative Type Theory multiplicities 0, 1, and omega; names Slake as the freestanding compiler product; requires a freestanding product wire without managed Lean runtime or garbage collection; requires CompCert verified compilation of that emit and bootstrapping a Slake compiler that fully typechecks as core validation steps. Cites RFC 2119 and SemVer from this repository's ref/, and cites 0000_spec.md at the repository root. Lean 4, Idris 2, CompCert, and Rust Form 1 pins live in the Systems Lean product tree, not this repository's ref/. Companion Lean meaning proofs live under lean/SystemsLean.lean and are not the numbered specification. The Smart Symbolic Supercompiler is specified in 0004_SSSSS.md. beastdb is specified in 0003_beastdb.md.
4. 0003_beastdb.md - beastdb, version 1.0.0. Defines the durable ordered store with lowercase product name beastdb and freestanding library libbeastdb; requires Systems Lean, a bootstrapped Slake that fully typechecks, and CompCert verified compilation as in 0002; requires proven ACID, tries that do not use locks, SWMR, optional access by more than one writer on disjoint leaves, fencing by generation, mmap, SIMD, zerocopy, LanguageID, WordID, Rosetta, mandatory schema with two modes, and interoperability through fargo rather than a traditional foreign function interface. This specification does not claim a conforming implementation exists. Companion Lean meaning proofs live under lean/BeastDb.lean. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
5. 0004_SSSSS.md - Surmount Systems Smart Symbolic Supercompiler, version 1.0.0. Defines encoding as sequential language runs with LanguageID prefix only on change; requires 64 bit sequential LanguageID and per language sequential WordID as primary identity and forbids hashing as primary identity; requires Rosetta relations with provenance tags; requires a deterministic pipeline given the same vocabulary and relation set; permits neural proposals only after reduction to sequential integers; permits natural language translation as work that is best effort and that must be marked provisional unless it is Lean proven or high confidence; requires durable state in beastdb and a Systems Lean core with CompCert and a Slake bootstrap that fully typechecks for components that are safety critical, that run in environments with tight resources, and that are freestanding. This specification does not claim a conforming implementation exists. Companion Lean meaning proofs live under lean/Sssss.lean. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
6. 0005_CATE.md - Concise American Technical English, version 1.1.0. First publication of CATE as a numbered specification. Requires complete American English thoughts, questions to humans that name file or clause, current wording, why it matters, options, ordinary English, a new phrase defined in the same sentence when one is introduced, and what we will do for each option, concise prose, leftover unstack as nonconforming, residual written in full, numbered markdown as the contract humans read, no invented conforming product, CATE as not a replacement for RFC 2119, independent work streams as parallel subagents, self improvement of the encode process in the same effort, and size reports that include COCOMO when the operator asked for size. This 1.1.0 also folds the Vocabulary catalog (formerly numbered specification 0009) into this specification. Number 0009 is withdrawn. Root VOCABULARY.md is a short pointer to this file. Other numbered specifications SHALL use these tokens as defined here when they use those words. Companion Lean meaning proofs live under lean/Cate.lean. Catalog encodings live under lean/VocabularySpec.lean. Proofs live under lean/VocabularyProofs.lean. Runtime isomorphism reads this file, not the pointer. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
7. 0006_RSI.md - Recursive Self Improvement, version 1.1.0. Defines a skill, a philosophy, and possible later input to the Surmount Systems System Prompt for Surmount numbered specifications and for agents that encode them. Requires durable tools over a disposable job, the best available tool that can state a theorem or a contract, a failing in-tree test for a named contract before the product edit that is meant to make that same test pass, stopping and asking on ambiguity, remaining work written in full on disk, and the self improvement loop of improving tools, proving them, and keeping residual honest. Keeps the same English word distinct when it names different trees (language versus compiler versus package id, spec versus meaning model versus form checker, remaining work versus a named freestanding blocker). CATE is not this specification. SSSP is not specified. Scripture named in that document is not a conformance item for Slake, beastdb, or SSSSS. This specification does not claim that every agent already conforms. Companion Lean meaning proofs live under lean/Rsi.lean and lean/Vocabulary.lean. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
8. 0007_CI.md - Continuous Integration and stack consistency, version 1.0.0. Requires the named gate green before commit and before push (this repository's gate is nix flake check "path:$PWD" --print-build-logs), commits signed by the human operator, and a ban on agents creating commit objects. Names one exception only for a product that keeps two source trees when that product's residual records unsigned history or history signed with a different key. Keeps numbered markdown, Lean spec encodings, Lean proofs, and product implementation distinct in this specifications repository. Records that Systems Lean product trees unify specification, proof, and implementation in one typed language. Requires byte identity of Slake emit for a conforming Systems Lean and Slake product and records that the match is not claimed done. Requires the SSSSS and beastdb reality check for that stack and records that the check is not claimed done. fargo remains unnumbered. This specification does not claim that a conforming Continuous Integration product exists. Companion Lean meaning proofs live under lean/Ci.lean. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
9. 0008_Formal_Vibefication.md - Formal Vibefication, version 1.0.0. Requires the specification to be encoded in Lean as declarations of what must be true, in modules marked as spec encodings. Requires proofs to live in separate Lean modules that import those encodings. Numbered markdown remains the contract humans read and is not a substitute for those encodings. Lean proofs are not the specification. spec_check remains form of numbered markdown. A mash of spec encodings and their proofs that hides the split is nonconforming in this specifications repository. Every published numbered markdown file has a sibling Spec_NNNN.lean at the repository root whose physical lines match that markdown, with proofs in lean/Proofs_NNNN.lean, checked by line_encodings_check. Systems Lean product trees may unify specification, proof, and implementation; mashing that home with this repository's split is False. Cites canonical Proof of Keags URLs and requires back linking. Number 0009 is withdrawn. The word catalog lives in CATE (0005_CATE.md). Meaning encodings live under lean/FormalVibeficationSpec.lean. Proofs live under lean/FormalVibeficationProofs.lean. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
10. 0010_Surmount_Systems.md - Surmount Systems, version 1.0.0. Human contract for how numbered specifications, Lean spec encodings, Lean proofs, and product paths fit. Cites Formal Vibefication as specification 0008 with canonical Proof of Keags URLs and requires back linking. Numbered markdown is the contract humans read; spec encodings are Lean; proofs are separate Lean modules. Every published numbered markdown file has a sibling Spec_NNNN.lean whose physical lines match that markdown. Systems Lean product trees unify specification, proof, and implementation, then Slake emits freestanding C ahead of time and MAY emit optional LLVM IR; that unification is not a license to mix encodings with proofs here or to mix theorems into numbered markdown here. The Lean module Surmount is the single composition proof (surmount_integrates and related). A mash of identities is False. beastdb, SSSSS, Slake, and Continuous Integration are ongoing and not ready for use. Byte identity of emit is required and not claimed true. Number 0009 is withdrawn. The word catalog lives in CATE (0005_CATE.md). fargo, SSSP, Carbonado, and Lean Machine remain unspecified. This specification does not claim a conforming product exists. Companion Lean lives under lean/Surmount.lean. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.

Domain words allowed by the spelling list are mapped in 0005_CATE.md. Root VOCABULARY.md is a short pointer. Companion Lean vocab_aspell_tests proves the catalog matches aspell_words.txt as an isomorphism of tokens and L_n ids. That map is not ISO 24495. Entry definitions remain human prose for meaning beyond the isomorphism. Number 0009 is withdrawn. The file 0009_VOCABULARY.md MUST NOT exist.

3. Document rules

All new specification prose SHALL follow 0000_spec.md. Summary for everyday use:

1. American English spelling and wording throughout (en_US).
2. Pure ASCII characters only (no Unicode punctuation or letters that are not ASCII). Use ASCII -, straight quotes, and ... (three periods). Files use line endings that use LF and never CR.
3. Prefer ordinary English over hyphenated compounds. Do not write lawyerly modifiers such as high-assurance, best-effort, self-improving, lock-free, or safety-critical. Do not "fix" them by deleting the hyphen and leaving the same two words (lock free, non markdown, must like, LF only). Rephrase so a person would actually say it. high assurance may stay when it already reads as English. 3 bit, 8 bit, 24 bit, and high contrast may stay. Say tries that do not use locks rather than lock free tries. Say bootstrapped Slake that fully typechecks rather than fully type checking Slake. Keep a hyphen only for filenames, URLs, code identifiers, and official designations (for example ITU-T). The automated checker fails on lowercase identifiers with two or more hyphens (three or more segments), for example foo-bar-baz. That mechanical ban is a floor. It does not license a single hyphen in prose when a rephrased form works, and it does not license deleting the hyphen and leaving the same two words. A single hyphen is still allowed by that mechanical checker; authors still should rephrase rather than leave a hyphen. The tool name pre-commit may stay as the tool name. Concise American Technical English (CATE) is specified in 0005_CATE.md (version 1.1.0). 0000_spec.md version 1.3.0 keeps a short pointer only. spec_check also flags the leftover unstack floor list in 0005_CATE.md (non markdown, must like, LF only, lock free tries, fully type checking) in numbered specification prose outside fences and inline code. It does not flag high assurance, 3 bit, or time series. Numbered specifications other than 0000 that contain a planned NNNN_*.md token must include a heading titled Residual. Number 0006 is Recursive Self Improvement (0006_RSI.md). CATE is not 0006.
4. Enumerate sections and lists clearly. Use numbered or lettered lists. Do not use markdown bullet markers (-, *, +) outside fenced code.
5. Do not wrap prose to a column. Prefer one physical line per paragraph and per list item body. Soft wrap is the reader's editor setting. Deliberate breaks stay for headings, blank lines, list items, tables, and fenced code.
6. Leading indentation uses tab characters only (not spaces). Spaces in the middle of a line and inside table cells are fine. Nested lists indent with tabs. No trailing spaces or tabs at end of line.
7. Maintain high precision. Label open questions and behavior the implementation defines. Do not leave silent gaps implementers need filled.
8. Name files NNNN_descriptive_name.md with a four digit prefix and underscores in the descriptive part (not filenames that use hyphens in the basename). Place them only in the repository root (not under a nested specs/ folder). 0000 is reserved for the spec spec (0000_spec.md).
9. Background, history, and design reasoning text is informative. Requirements use RFC 2119 keywords (MUST, SHALL, SHOULD, MAY, and related words) in the RFC 2119 sense. Informative sections should be titled or opened so readers can tell they are not requirements (for example "Algorithm selection reasoning"). Do not invent private requirement jargon; use ordinary English plus RFC 2119. An RFC 2119 keyword still makes a sentence normative even inside an otherwise informative section; prefer keeping requirements in normative sections.
10. Every normative spec includes a Required Conformance clause (how to conform to that spec). Meeting the form rules in 0000 is a separate checklist in that document ("Conformance to this document").
11. Include Copyright or License text, or state that the repository Unlicense applies.

Standard legal text in UNLICENSE.md is excluded from style, spelling, list, and hyphenation checks.

4. Versioning and publication

1. Specs use real Semantic Versioning (SemVer) 2.0.0: MAJOR.MINOR.PATCH. Cite SemVer; local copy path when present: ref/semver.
2. The repository operator controls when a specification is published.
3. Do not invent pretend shipped releases or a 0.x release train for work that was never published.
4. First publication of a specification SHALL be version 1.0.0.
5. Specs MAY carry a SemVer version line (see the pattern in 0000). A version line of 1.0.0 on a current file is the version on disk. It is not by itself a claim that the operator has declared publication. Do not invent fake version history or claim publication the operator has not declared.
6. After publication, incompatible changes raise MAJOR; backward compatible additions raise MINOR; compatible fixes raise PATCH, as SemVer describes.
7. The Lean tool spec_check has its own SemVer, independent of SemVer for numbered specifications. A bump to the tool does not imply a bump to 0000_spec.md or any other numbered specification, and the reverse is also true. The tool is at 1.0.0 as its first intentional tool release.

5. RFC 2119 requirement keywords

Specs SHALL use RFC 2119 keywords in the RFC 2119 sense:

MUST, MUST NOT, REQUIRED, SHALL, SHALL NOT, SHOULD, SHOULD NOT, RECOMMENDED, MAY, OPTIONAL.

Cite RFC 2119 (local path when present under ref/, for example ref/rfc2119). Uppercase keywords in normative clauses are recommended for scanability. Do not invent a private rule that bans MUST or redefines these words. Background and design reasoning prose is informative; label such sections clearly. See 0000_spec.md Clause 4.2.

6. External references (ref/)

ref/ holds the external standards this repository cites so readers and tools can open the exact text meant without hunting the web. Hyperlinks to publisher pages still matter; canonical URLs stay in SOURCE and in citations. Local copies freeze what was reviewed and checksummed or pinned in git. Full process, reasoning, and per-entry license notes: ref/README.md. Normative summary: 0000_spec.md Clause 12.

1. Binding rule: any external specification this repository cites MUST be present under ref/ in one of two honest forms:
   1. Form 1: Canonical git that the publisher maintains. Git submodule from the publisher's canonical git repository (any host, not assumed GitHub), pinned to a tag or commit.
   2. Form 2: No canonical git that the publisher maintains. Keep a local copy of the specific official publisher artifact (PDF, plain text, or similar) under ref/<name>/, committed directly in this repository's git tree (ordinary files, not a submodule), with a SOURCE file (canonical URL, retrieval date, checksum, edition or version). Form 2 is used when the publisher does not maintain canonical git. In ref/README.md you must say that there is no publisher git, record license and copyright, and record why Form 2 was used. Hyperlinks to the publisher still matter as publisher links. That form does satisfy the rule and is the intentional process for standards from before git and from the PDF era (RFC 2119, ECMA-48, ITU-T T.416, similar), not a fallback failure.
2. Prefer honesty: never invent a third party mirror or community reformat as "canonical git." Prefer Form 1 when the publisher truly maintains git for that standard; Form 2 when that is what the publisher ships.
3. Adding a new external citation in a spec requires adding or updating the matching ref/ entry under that process.
4. Present entries (all valid under the rule above):
   1. SemVer (ref/semver) - Form 1 git submodule of https://github.com/semver/semver , pinned to tag v2.0.0 (commit 7c834b3f3a4940d77ab593bc32583004d6a426a9). Upstream doc license: CC BY 3.0. See ref/semver.SOURCE and ref/README.md.
   2. RFC 2119 (ref/rfc2119) - Form 2 official RFC Editor plain text, committed directly in this tree (not a submodule), with SOURCE. Canonical publication is https://www.rfc-editor.org/rfc/rfc2119.txt ; there is no canonical git that the publisher maintains for this historic RFC. IETF Trust / RFC copyright; freely available from the RFC Editor; Surmount does not own the text. See ref/rfc2119/SOURCE and ref/README.md.
   3. ECMA-48 (ref/ecma48) - Form 2 official Ecma International PDF, committed directly in this tree (not a submodule), with SOURCE. Ecma text copyright policy allows unchanged republication with notice. Community reformats are not the Ecma publisher source. See ref/ecma48/SOURCE and ref/README.md.
   4. ITU-T T.416 / ISO/IEC 8613-6 (ref/itu_t416) - Form 2 official ITU free PDF (Recommendation T.416, 03/93; identical text also published as ISO/IEC 8613-6), committed directly in this tree (not a submodule), with SOURCE. No canonical git that the publisher maintains. Surmount does not own the text. See ref/itu_t416/SOURCE and ref/README.md.
5. Paths may be documented before the directories are populated. Empty paths are not an excuse to drop the public citation.
6. git submodule add has no --dry-run. Preflight a new Form 1 submodule with git ls-remote <url> and an optional temporary clone outside the tree.
7. After this repository has its first commit with submodule gitlinks, clones populate Form 1 submodules with:

git submodule update --init --recursive

Or clone with `git clone --recurse-submodules <url>`. Those commands apply only to real Form 1 submodules (for example `ref/semver`). Form 2 pins such as `ref/rfc2119`, `ref/ecma48`, and `ref/itu_t416` are ordinary files in this repository's git tree and need no submodule init.

8. The Lean 4 agent skill pack is a git submodule at skills/lean4-skills. It is not a Clause 12 pin and is not under ref/. After clone, populate it with:

git submodule update --init skills/lean4-skills

`git submodule update --init --recursive` also initializes Form 1 pins such as `ref/semver` together with this pack.

7. Validation (Lean and Nix)

7.1 Local and CI gate (Nix is primary)

Nix is the primary interface for validation. There is no scripts/ bash gatekeeper. The canonical command for local work and GitHub Actions is:

nix flake check "path:$PWD" --print-build-logs

CI installs Nix and runs that command directly (workflow: .github/workflows/check.yml). Checkout initializes Form 1 git submodules; Form 2 pins need no submodule init. It does not install or invoke just.

just is optional local sugar only. just check runs the same Nix flake check line; you do not need just if you call Nix yourself. Prefer path: when local flake files may be untracked so pure git tree eval is not required.

On a single architecture host, nix flake check may warn that it omitted checks for incompatible systems. That omit warning is normal and not a failure.

What the flake checks cover (separate checks; nix flake check runs all of them):

1. checks.spec_check - Lean form rules and American English spelling on numbered specifications at the repository root, plus the registry scan for numbered specifications (files that must exist at the root include 0005_CATE.md, 0006_RSI.md, 0007_CI.md, 0008_Formal_Vibefication.md, and 0010_Surmount_Systems.md; a stale 0005_fargo.md token must fail; withdrawn 0009_VOCABULARY.md must fail; the Lean field named published means the file must exist, not that the operator has declared a SemVer publication; NNNN_name.md tokens must match the registry, product name beastdb must stay lowercase), plus CATE leftover unstack phrases from 0005_CATE.md, a Residual heading when a numbered specification other than 0000 contains a planned file token (0000 is exempt), and a numbered specification that names Keagan or proofofkeags must also contain proofofkeags.com. Thin runCommand puts the packages.spec_check binary and pkgs.aspellWithDicts on PATH, sets REPO_ROOT, and runs spec_check. No discovery or aspell loops in shell; spelling is inside Lean. The registry lives in lean/SpecRegistry.lean.
2. checks.whitespace - pure Nix evaluation of text owned by the project for trailing whitespace and leading indent that uses tabs only (skips vendor blobs under ref/semver, PDFs, and RFC plain text; Lean and YAML may indent with spaces). Violations that are not empty fail evaluation with throw; success is a writeText marker with no shell. No bash script.
3. checks.pre-commit-check - sandboxed pre-commit suite (Lean hook on numbered specifications only; spelling rides along when aspell is on PATH from the dev shell). Whitespace across the project is the pure Nix flake check, not a bash pre-commit hook.
4. checks.spec_check_tests - hermetic Lean unit tests for spec_check form rule helpers (string fixtures).
5. checks.systems_lean_tests - companion meaning proofs for 0002_Systems_Lean.md (multiplicities, finite use counts for erased / linear / affine / unrestricted, composed Clause 5 conformance, language set, hygiene including product tree ref/ names, and stack targeting claims). Clause 5 conformance on the wire holds when the product is freestanding, has no managed Lean runtime, and has no garbage collection, or when every leftover that still blocks that is named and tracked. CompCert verified compilation and a bootstrapped Slake that fully typechecks are separate Clause 5 items; a named leftover does not excuse either. This is not a second markdown form checker. The Smart Symbolic Supercompiler is specification 0004 in that model, not 0003. beastdb is specification 0003.
6. checks.beastdb_tests - companion meaning proofs for 0003_beastdb.md (lowercase product name, libbeastdb, Systems Lean and Slake bootstrap typecheck, proven ACID and tries that do not use locks as required, mandatory schema with two modes, fargo rather than a traditional foreign function interface, scope of a store that is local first, stack numbers) plus registry string fixtures. This is not a second markdown form checker.
7. checks.sssss_tests - companion meaning proofs for 0004_SSSSS.md (sequential WordID rather than hashing as primary identity, LanguageID prefix only on change, Rosetta provenance tags, pipeline determinism, neural proposals reduced to sequential integers, natural language translation marked provisional unless proven or high confidence, durable state in beastdb, Systems Lean file 0002_Systems_Lean.md) plus registry string fixtures. This is not a second markdown form checker.
8. checks.cate_tests - companion meaning proofs for Concise American Technical English as specification 0005 (not specification 0006, not an extension clause of 0000): leftover unstack is nonconforming, residual silence is nonconforming, questions to humans must carry file, wording, why, options, ordinary English, a new phrase defined in the same sentence when one is introduced, and what we will do for each option. This is not a second markdown form checker.
9. checks.rsi_tests - companion meaning proofs for 0006_RSI.md (RSI is specification 0006, CATE is 0005, fargo is not 0005, SSSP is not specified, durable tools before a disposable job, leftover unstack still fails, vocabulary mappings so the same English word in different trees is a type error if mashed). This is not a second markdown form checker.
10. checks.ci_tests - companion meaning proofs for 0007_CI.md (CI is specification 0007, not 0005 and not 0006; unsigned commit without the named exception does not conform; commit on a red gate does not conform; numbered markdown, meaning model, and product implementation stay separate in this repository; Systems Lean product trees unify those three; byte identity of emit is required and not claimed true; SSSSS and beastdb reality check is required and not claimed done; fargo is unspecified). This is not a second markdown form checker.
11. checks.vocab_aspell_tests - isomorphism between root aspell_words.txt and 0005_CATE.md catalog headings: same set of tokens, exactly one L_n id per token, ids L_1 through L_k with no gaps, sort by ASCII without regard to case then by ASCII code on a tie. Thin runCommand sets REPO_ROOT and runs the Lake executable vocab_aspell_tests. Root VOCABULARY.md is a pointer. This is not ISO 24495. Number 0009 is withdrawn; 0009_VOCABULARY.md MUST NOT exist.
12. checks.formal_vibefication_tests - spec encodings and separate proofs for Formal Vibefication as specification 0008 (lean/FormalVibeficationSpec.lean and lean/FormalVibeficationProofs.lean): a mashed module that holds encodings and their proofs does not conform; separate marked modules do conform; number 0008 is published; number 0009 is withdrawn. This is not a second markdown form checker.
13. checks.surmount_tests - composition proof over the meaning models (lean/Surmount.lean), cited by numbered specification 0010_Surmount_Systems.md: unique stack numbers, CATE is 0005, RSI is 0006, CI is 0007, Formal Vibefication is 0008, the word catalog is owned by CATE as 0005, number 0009 is withdrawn, SSSSS is 0004, beastdb is 0003, Systems Lean is 0002, Surmount Systems is 0010, fargo unassigned, SSSP unspecified, leftover unstack nonconforming, Lean spec encodings are CATE on the leftover unstack floor, byte identity required and not claimed true, products ongoing and not ready for use, this repository keeps spec encodings distinct from proofs and from markdown form, Systems Lean product trees may unify spec, proof, and implementation, every published numbered markdown file has a sibling Spec_NNNN.lean, and the Keagan backlink rule exists. Treating this repository's split and product tree unification as the same layer is inconsistent. Mash of 0009 as published is false. This is not a second markdown form checker and is not a proof that Slake emit already matches ELF.
14. checks.line_encodings_tests - hermetic Lean unit tests for physical line splitting and isomorphism of markdown lines versus Lean encodings, including leftover unstack fixtures on compiled encodings and spec encoding comments. This is not a second markdown form checker.
15. checks.line_encodings_check - Lean program line_encodings_check reads each root NNNN_*.md and the compiled lines from sibling Spec_NNNN.lean and fails when a markdown line has no encoding or an encoding has no matching markdown line. It also fails when that sibling contains include_str. The encoding is explicit Lean MdLine or String literals, one per physical markdown line. include_str is not a line encoding. Compiled encodedLines still must match the markdown bytes (LF lines). It fails when compiled encodedLines contain leftover unstack phrases in prose outside fenced code and inline code, and when comments in lean/FormalVibeficationSpec.lean or lean/VocabularySpec.lean contain those leftover phrases, using Cate.leftoverUnstackPhrases and the same leftover unstack scan as spec_check. That leftover unstack check is a floor, not a complete English checker. Thin runCommand sets REPO_ROOT and runs the binary. Proofs of those encodings live in lean/Proofs_NNNN.lean. spec_check discovery remains NNNN_*.md only; Spec_NNNN.lean is not a numbered specification. This is not a second markdown form checker.
16. checks.word_stats_tests - hermetic Lean unit tests for unique ASCII letter token tracking: lowercase fold, beastdb as one token, RFC as rfc, digits are not words, proven tokens from the CATE L_n catalog plus RFC 2119 requirement keywords already named as vocabulary, and percent math. This is not a second markdown form checker.
17. checks.word_stats - Lean program word_stats reads root numbered NNNN_*.md files plus README.md, AGENTS.md, RESIDUAL.md, and VOCABULARY.md, parses CATE catalog headings from 0005_CATE.md, and fails when root WORD_STATS.md is missing or stale. Proven tokens are lowercased CATE L_n entries plus RFC 2119 requirement keywords already named in 0000_spec.md Clause 4.1. That is not a second CATE catalog. This tracking is not a proof that every English sentence is CATE. The leftover unstack floor remains a separate check. Lean comments are not in the scan. Vendor trees under ref/, the Lean 4 skill pack, Lake build output, Nix result links, and git metadata are not in the scan. Thin runCommand sets REPO_ROOT and runs the binary. word_stats --write refreshes the report.

Numbered specifications matched for Lean and spelling:

1. Glob at repository root: [0-9][0-9][0-9][0-9]_*.md
2. Basename regex: ^[0-9]{4}_[A-Za-z0-9_]+\.md$
3. Examples: 0000_spec.md, 0001_DOGE.md, 0002_Systems_Lean.md, 0003_beastdb.md, 0004_SSSSS.md, 0005_CATE.md, 0006_RSI.md, 0007_CI.md, 0008_Formal_Vibefication.md, 0010_Surmount_Systems.md
4. Not in the default scan: README.md, AGENTS.md, UNLICENSE.md, and anything under subdirectories

Optional convenience: just with no arguments lists recipes (just --list / just -l). See the root justfile.

7.2 Authoritative checkers (Lean form rules and spelling; pure Nix whitespace)

Lean (lean/ binary spec_check, packaged as the default flake package and the default app) is authoritative for mechanical form rules and American English spelling on numbered specifications. Hermetic test binaries are extra packages, not extra apps. Tool SemVer for spec_check is independent of SemVer for numbered specifications; the tool is at 1.0.0 as its first intentional tool release (see section 4).

Dual whitespace (both stay on purpose)

Surface	Who enforces it	Why it stays
Trailing whitespace and leading indent that uses tabs only on numbered specifications	Lean spec_check (form suite; pre-commit and checks.spec_check)	Same binary as ASCII, bullets, hyphenation, wrapping to a column, spelling; line diagnostics for authors
Same class of rules on Surmount authored text across the tree	Pure Nix checks.whitespace (nix/whitespace.nix)	Evaluation gate without a process; no second language; covers README, AGENTS, flake, SOURCE pins, not only specs
Overlap on numbered specifications	Both run on nix flake check	Intentional. Do not drop Lean whitespace "because Nix covers the tree," and do not move whitespace across the tree into Lean "for symmetry." Rationale: section 7.2.1

Lean coverage on numbered specifications:

1. Pure ASCII (tab, LF, printable 0x20-0x7E; no CR or high bytes).
2. No markdown bullet list markers (-, *, +) outside fenced code.
3. No excess hyphenated tokens in prose (lowercase token with two or more hyphens, for example foo-bar-baz), ignoring fenced code, inline code, and URLs.
4. In scope specs (NNNN_*.md with the naming scheme above) must cite RFC 2119 (or RFC2119). README is not required to carry that citation. License files are style excluded for bullets, hyphenation, and RFC (ASCII and whitespace still checked).
5. No trailing whitespace (space or tab before end of line).
6. No leading indent with spaces (use tabs for nested markdown indent).
7. No prose wrapped to a column on numbered specifications (heuristic outside fences and tables; see 0000_spec.md Clause 6.4).
8. American English spelling via aspell list --lang=en_US --mode=markdown with personal dictionary aspell_words.txt (pure hex and pure digit tokens skipped). Requires aspell with en_US on PATH; flake checks.spec_check and nix develop supply pkgs.aspellWithDicts. Skip with SPECS_SPELLING=0 or SPECS_SKIP_SPELLING=1. There is no separate checks.spelling and no nix/spelling-check.nix.
9. CATE leftover unstack phrases in numbered specification prose outside fences and inline code (floor list in 0005_CATE.md Clause 3.5: non markdown, must like, LF only, lock free tries, fully type checking). Does not flag high assurance, 3 bit, or time series.
10. A Residual heading when a numbered specification other than 0000 contains a planned or unpublished NNNN_*.md token (0003 and 0004 already have Clause 6 Residual). 0000 is the form spec and is exempt.
11. A numbered specification that names Keagan or proofofkeags must also contain proofofkeags.com (back linking). The URL may sit on a later line than the name.

Whitespace across the project is a separate pure Nix check (nix/whitespace.nix, flake output checks.whitespace). It is not bash and not Lean.

1. Same trailing whitespace and leading space rules on Surmount authored text (*.md, *.nix, SOURCE pins we write, and similar).
2. Skips vendor material: ref/semver/**, *.pdf, ref/**/rfc2119.txt.
3. Lean (.lean) and YAML (.yml / .yaml) are exempt from the leading space ban because those languages reject tab indent. They still must not have trailing whitespace.
4. On nix flake check, a violation list that is not empty fails Nix evaluation (throw with all messages). Success uses pkgs.writeText (no shell builder). Debug with nix eval "path:$PWD#lib.whitespaceViolations".

Use pkgs.aspellWithDicts (English dictionaries bundled with the aspell wrapper). Bare nix shell nixpkgs#aspell or pairing aspell with aspellDicts.en as separate packages is not enough: aspell will report that no word lists can be found for en_US.

With no paths, spec_check discovers only numbered specifications at the root (same naming scheme).

Author tips for wrapping to a column

The Lean heuristic for wrapping to a column (normative algorithm in 0000_spec.md Clause 6.4) fails when two consecutive body lines that are not empty look like a wrap in the middle of a sentence: the first line does not end with ., !, ?, or :, and the next line starts with a lowercase letter. Fenced code and table rows are exempt.

What usually trips it:

1. A paragraph broken for column width so the continuation starts with a lowercase word on the next physical line.
2. A list item body split the same way across two physical lines.

How to fix:

1. Join each paragraph (and each list item body) into one physical line. Let the editor soft wrap.
2. Keep deliberate structure breaks: blank lines between paragraphs, one list item per line, headings, fences, tables.
3. A short full sentence that ends with . on its own line is fine even when the next line starts a new sentence with a capital letter.

Example that fails the heuristic (do not write this in numbered specifications):

This sentence was broken for column width in the middle
of a thought and the next line starts lowercase.

Example that passes (one physical line per paragraph; shown wrapped only in this README for display if your viewer wraps):

This sentence stays on one physical line so soft wrap is the reader's choice.

7.2.1 Why Lean vs pure Nix

This section records the design reasoning so future contributors do not "simplify" the wrong layer.

Short answer: pure Nix is right for simple rules across the tree that need no extra process. Lean is right for the form suite on numbered specifications and for anything that must run an external program (aspell). The flake is the interface; bash and Python are not check implementations.

Concern	Pure Nix?	Where it lives
Trailing whitespace / tab leading indent (whole tree)	Yes	nix/whitespace.nix, checks.whitespace
ASCII, bullets, hyphenation, RFC 2119 cite, wrapping to a column on NNNN_*.md	Possible, not chosen	Lean spec_check (maintainability)
Spelling with aspell	No as pure eval	Lean calls aspell on PATH
Fat shell/python loops in runCommand or scripts/	Forbidden	Never

Why pure Nix for whitespace across the project

1. The rule set is small (trailing space/tab; leading space ban with known exemptions).
2. Implementation needs only fileset discovery, readFile, and line scans.
3. Evaluation is the check: empty list plus writeText success, or throw with diagnostics. No builder shell, no second language.

Why Lean for form rules on numbered specifications and spelling

1. Spelling cannot be pure Nix evaluation. Pure eval does not spawn processes. Automated en_US spelling needs aspell. Acceptable shapes: a real binary that calls it (current Lean path), or drop spelling from the gate. Unacceptable: multi line bash/python policy inside a derivation builder.
2. Form rules beyond whitespace are a small linter (fence tracking, strip inline code and URLs, excess hyphenated tokens, heuristic for wrapping to a column, RFC citation). Those can be written in pure Nix the same way whitespace is, but they become long, slow to evaluate, and hard to test and debug in the evaluator. A packaged program with line diagnostics fits pre-commit and local authoring.
3. One binary owns the suite for numbered specifications (discovery of root NNNN_*.md, form rules, optional spelling skip via env). Nix packages it and runs a thin check; check policy does not live in shell strings.
4. Flake stays idiomatic: default package and app are the Lean spec_check binary; hermetic test binaries (spec_check_tests, systems_lean_tests, beastdb_tests, sssss_tests, cate_tests, rsi_tests, ci_tests, vocab_aspell_tests, formal_vibefication_tests, surmount_tests, line_encodings_tests, word_stats_tests) and the line encoding checker line_encodings_check and the word tracking checker word_stats are extra packages. Checks are pure whitespace plus thin invoke of those binaries plus pre-commit. No writeShellApplication gatekeeper packages.

What not to do without an explicit decision

1. Do not implement flake checks as bash or Python stuffed inside Nix (writeShellApplication, scripts/ checkers, shell strings that span multiple lines as check policy). Form rules for numbered specifications live in the Lean spec_check binary. Trailing whitespace and tab indent across the tree live in pure Nix evaluation.
2. Do not move whitespace across the tree into Lean only for symmetry with form rules.
3. Do not assume "everything should be pure Nix" or "everything should be Lean." Match the rule to the mechanism: pure data rules to pure Nix; form policy that needs a process or that takes more than one pass to the Lean binary (or another real language package if the operator chooses to replace Lean later).

Agent facing copy of this split: AGENTS.md (Machine validation / Why Lean vs pure Nix). Keep both in sync when the authority model changes.

7.3 Run Lean directly

With lean / lake from nixpkgs (or nix develop):

cd lean && lake build
./.lake/build/bin/spec_check
./.lake/build/bin/spec_check 0000_spec.md 0001_DOGE.md 0002_Systems_Lean.md 0003_beastdb.md 0004_SSSSS.md 0005_CATE.md 0006_RSI.md 0007_CI.md 0008_Formal_Vibefication.md 0010_Surmount_Systems.md
lake build systems_lean_tests
./.lake/build/bin/systems_lean_tests
lake build beastdb_tests
./.lake/build/bin/beastdb_tests
lake build sssss_tests
./.lake/build/bin/sssss_tests
lake build cate_tests
./.lake/build/bin/cate_tests
lake build rsi_tests
./.lake/build/bin/rsi_tests
lake build ci_tests
./.lake/build/bin/ci_tests
lake build vocab_aspell_tests
REPO_ROOT=.. ./.lake/build/bin/vocab_aspell_tests
lake build surmount_tests
./.lake/build/bin/surmount_tests
lake build formal_vibefication_tests
./.lake/build/bin/formal_vibefication_tests
lake build line_encodings_tests
./.lake/build/bin/line_encodings_tests
lake build line_encodings_check
REPO_ROOT=.. ./.lake/build/bin/line_encodings_check
lake build word_stats_tests
./.lake/build/bin/word_stats_tests
lake build word_stats
REPO_ROOT=.. ./.lake/build/bin/word_stats

Or via the flake (default package and default app are both the Lean binary):

nix build "path:$PWD#spec_check" -L
nix run "path:$PWD#spec_check"
nix run "path:$PWD#spec_check" -- 0000_spec.md

Exit status is nonzero when any check fails. Diagnostics go to stderr as file:line: message.

7.4 Run via Nix

# Canonical gate (local and CI): all flake checks
nix flake check "path:$PWD" --print-build-logs
# Optional sugar (same command):
just check
# Lean binary only:
nix run "path:$PWD#spec_check"
nix build "path:$PWD#spec_check" -L
# Individual checks (system name varies):
nix build "path:$PWD#checks.$(nix eval --impure --raw --expr builtins.currentSystem).spec_check" -L
nix build "path:$PWD#checks.$(nix eval --impure --raw --expr builtins.currentSystem).whitespace" -L

Flake layout:

1. packages: spec_check (Lean form checker binary, including the registry scan for numbered specifications; also default), plus hermetic test binaries spec_check_tests, systems_lean_tests, beastdb_tests, sssss_tests, cate_tests, rsi_tests, ci_tests, vocab_aspell_tests, surmount_tests, formal_vibefication_tests, line_encodings_tests, and word_stats_tests, plus the line encoding checker line_encodings_check and the word tracking checker word_stats.
2. apps: only spec_check (also default -> same binary path).
3. checks: spec_check (form rules + spelling + registry scan + CATE leftover unstack and residual heading + Keagan back linking), spec_check_tests, systems_lean_tests (0002 meaning proofs, not form rules), beastdb_tests (0003 meaning proofs and registry fixtures, not form rules), sssss_tests (0004 meaning proofs and registry fixtures, not form rules), cate_tests (0005 CATE meaning proofs, not form rules), rsi_tests (0006 RSI meaning proofs, not form rules), ci_tests (0007 CI meaning proofs, not form rules), vocab_aspell_tests (aspell list and 0005_CATE.md catalog inverse maps), formal_vibefication_tests (0008 spec encodings versus proofs, not form rules), surmount_tests (composition proof over those models, not form rules), line_encodings_tests (hermetic line encoding fixtures, not form rules), line_encodings_check (isomorphism of numbered markdown lines and sibling Spec_NNNN.lean encodings; include_str is not a line encoding; leftover unstack floor on compiled encodings and named spec encoding comments; not form rules), word_stats_tests (hermetic unique word tracking fixtures, not form rules), word_stats (root WORD_STATS.md matches unique English word counts versus the CATE catalog; tracking, not a complete English proof), whitespace, pre-commit-check (each independent; no bash orchestrated aggregate package).
4. No writeShellApplication packages and no scripts/ validation tools.

7.5 Systems Lean meaning proofs (not form rules)

Numbered specification 0002_Systems_Lean.md is the contract that humans read. Companion Lean modules under lean/SystemsLean.lean encode selected checkable claims from that spec: the multiplicity set {0, 1, omega}, erasure of multiplicity 0 at compile time, a finite use count model for linear (exactly once), affine (at most once), erased (zero runtime uses), and unrestricted (any Nat of uses), a freestanding product wire with no managed Lean runtime and no garbage collection, residual honesty composed with that wire (Clause 5 item 2: a freestanding product with no managed Lean runtime and no garbage collection, or every remaining blocker named and tracked), CompCert verified compilation and a bootstrapped Slake that fully typechecks as required Clause 5 conjuncts (a named residual does not excuse either), the novel language set (Idris 2, Lean 4 including Systems Lean, and pure Nix), Unlicense vs upstream ref/ hygiene with product tree directory names Idris2, lean4, CompCert, and rust, stack targeting as a claim that fails when a Clause 4.4 component cannot target Slake, one Clause 5 conformance predicate over those facts, and the fact that this specification is number 0002 (the Smart Symbolic Supercompiler is specified in 0004_SSSSS.md, not 0003; beastdb is specified in 0003_beastdb.md). Optional LLVM IR emission is modeled and is not required for conformance.

Those modules are meaning proofs. They do not replace the markdown spec. They do not duplicate spec_check form rules (ASCII, tabs, RFC 2119 citation, spelling, wrapping to a column, hyphenation, bullets). Form checking remains checks.spec_check. Meaning model tests are checks.systems_lean_tests (Lake executable systems_lean_tests).

This is the same split described in Clause 1.2 of 0002_Systems_Lean.md and in 0008_Formal_Vibefication.md: numbered markdown is the contract that humans read; the specification is also encoded in Lean as declarations of what must be true; proofs of those encodings live in separate Lean modules; Lean proofs are not the specification.

7.6 beastdb meaning proofs and the number registry

Numbered specification 0003_beastdb.md is the contract that humans read for beastdb. Companion Lean modules under lean/BeastDb.lean encode selected checkable claims from that spec: the lowercase product name beastdb, the library name libbeastdb, Systems Lean plus a bootstrapped Slake that fully typechecks and CompCert as required, proven ACID and tries that do not use locks as required, SWMR required with more than one writer on disjoint leaves optional, mandatory schema with predefined and inferred modes, interoperability through fargo and not a traditional foreign function interface, the scope of a store that is local first with network features out of scope, Carbonado unassigned, and this specification as number 0003 (not 0002, not 0004). Those modules are meaning proofs. They do not replace the markdown spec. Meaning model tests are checks.beastdb_tests (Lake executable beastdb_tests).

The registry for numbered specifications is lean/SpecRegistry.lean. It encodes rows whose files must exist (0000 spec spec, 0001 DOGE, 0002 Systems Lean, 0003 beastdb, 0004 SSSSS, 0005 CATE, 0006 RSI, 0007 CI, 0008 Formal Vibefication, 0010 Surmount Systems). Planned rows are empty. Number 0009 is withdrawn. The Lean field named published on those ten rows means the file must exist. It does not mean the operator has declared publication of those specifications. Theorems pin unique numbers, beastdb = 3, Systems Lean = 2, SSSSS = 4, CATE = 5, RSI = 6, CI = 7, Formal Vibefication = 8, vocabulary ownership = 5 (equals CATE), Surmount Systems = 10, fargo unassigned, SSSP unassigned, Lean Machine unassigned, and Carbonado unassigned. spec_check runs an IO scan of root NNNN_*.md files so a wrong number, a file name mismatch, a stale 0005_fargo.md token, a withdrawn 0009_VOCABULARY.md file, or a wrong capitalization of beastdb fails checks.spec_check and therefore nix flake check. Registry string fixtures also run in checks.beastdb_tests, checks.sssss_tests, checks.cate_tests, checks.rsi_tests, checks.ci_tests, checks.formal_vibefication_tests, and checks.surmount_tests. Tests that every published file is present use publishedBasenames from that registry so a new published row does not require a hardcoded list in each suite.

7.7 SSSSS meaning proofs (not form rules)

Numbered specification 0004_SSSSS.md is the contract that humans read for SSSSS. Companion Lean modules under lean/Sssss.lean encode selected checkable claims from that spec: this specification as number 0004 with file name 0004_SSSSS.md, Systems Lean as 0002, beastdb as 0003, RSI as 0006, fargo as not specification 0005, sequential WordID rather than hashing as primary identity, LanguageID prefix only on language change, a language run as LanguageID plus a WordID list, Rosetta provenance tags, pipeline determinism given the same vocabulary and relation set, durable state in beastdb, neural proposals reduced to sequential integers before acceptance, natural language translation marked provisional unless proven or high confidence, CompCert and a Slake bootstrap that fully typechecks for components that are safety critical with residual honesty not substituting, and the fact that a stale Systems Lean file name 0003_systems_lean.md fails. Those modules are meaning proofs. They do not replace the markdown spec. Meaning model tests are checks.sssss_tests (Lake executable sssss_tests). This specification does not claim a conforming implementation exists. Lean Machine has no numbered specification.

7.8 CATE meaning proofs (not form rules)

Numbered specification 0005_CATE.md is the contract that humans read for Concise American Technical English. It is numbered specification 0005. It is not numbered specification 0006. Number 0006 is Recursive Self Improvement (0006_RSI.md). 0000_spec.md version 1.3.0 keeps a short pointer only and does not restate CATE. Companion Lean modules under lean/Cate.lean encode selected checkable claims: CATE is specification 0005 with file name 0005_CATE.md (and CATE is not specification 0006), leftover unstack is nonconforming, residual silence is nonconforming, planned file tokens in numbered specifications other than 0000 require a Residual heading while 0000 is exempt, questions to humans must carry file or clause, current wording, why it matters, options, ordinary English, a new phrase defined in the same sentence when one is introduced, and what we will do for each option, spec markdown is the contract humans read, meaning proofs are not a second form checker, ISO 24495-1:2023 and the US Federal Plain Language Guidelines are not Clause 12 pins, CATE does not replace RFC 2119, independent work streams run in parallel, and the encode process self improves in the same effort. Those modules are meaning proofs. They do not replace the markdown spec. Meaning model tests are checks.cate_tests (Lake executable cate_tests). Leftover unstack scanning and the Residual heading check remain spec_check form rules.

ISO 24495-1:2023 Plain language and the US Federal Plain Language Guidelines (https://www.plainlanguage.gov/, accessed: 2026-08-25) are informative prior art. They are not 0000 Clause 12 pins. This repository does not keep them under ref/.

7.9 RSI meaning proofs (not form rules)

Numbered specification 0006_RSI.md is the contract that humans read for Recursive Self Improvement. Companion Lean modules under lean/Rsi.lean and lean/Vocabulary.lean encode selected checkable claims from that spec: this specification as number 0006 with file name 0006_RSI.md, CATE as specification 0005 and not specification 0006, fargo as not specification 0005, SSSP as not specified, durable tools before a disposable job, leftover unstack still nonconforming, scripture not a conformance item for Slake, beastdb, or SSSSS, bitmask trees out of scope as product, and vocabulary mappings so Systems Lean, Slake, and the Lake package id SystemsLean are different types, numbered markdown is not the meaning model and not spec_check, remaining work on disk is not Systems Lean residual and not a product tree claim that a freestanding release has no managed Lean leftover, leftover unstack stays CATE, the ASCII word omega maps to the Lean constructor unrestricted, independent streams with disjoint writes run in parallel, and a failing test then a product edit conforms while reshaping a test after the product edit does not. Those modules are meaning proofs. They do not replace the markdown spec. Meaning model tests are checks.rsi_tests (Lake executable rsi_tests). This specification does not claim that every agent already conforms.

7.10 CI meaning proofs (not form rules)

Numbered specification 0007_CI.md is the contract that humans read for Continuous Integration and stack consistency. It is not numbered specification 0005. It is not numbered specification 0006. Companion Lean modules under lean/Ci.lean encode selected checkable claims: this specification as number 0007 with file name 0007_CI.md, an unsigned commit without the named exception as nonconforming, a commit while the named gate is red as nonconforming, numbered markdown and the meaning model and product implementation as three distinct layers in this specifications repository, the Systems Lean product path as unification of those three in product trees, byte identity of emit as required for product conformance and not claimed true, the SSSSS and beastdb reality check as required for that stack and not claimed done, fargo as unspecified and not specification 0007, CATE as specification 0005, and RSI as specification 0006. Those modules are meaning proofs. They do not replace the markdown spec. Meaning model tests are checks.ci_tests (Lake executable ci_tests). This specification does not claim that a conforming Continuous Integration product exists. Byte identity of Slake emit is not claimed done.

7.11 Formal Vibefication spec encodings and proofs (not form rules)

Numbered specification 0008_Formal_Vibefication.md is the contract that humans read for Formal Vibefication. It is numbered specification 0008. Number 0009 is withdrawn. The word catalog lives in CATE (0005_CATE.md). Lean spec encodings under lean/FormalVibeficationSpec.lean state what must be true. Lean proofs under lean/FormalVibeficationProofs.lean import that module and establish those propositions. A mashed module that holds encodings and their proofs does not conform. Separate marked modules do conform. Every published numbered markdown file has a sibling Spec_NNNN.lean at the repository root. Proofs of those line encodings live in lean/Proofs_NNNN.lean. Numbered markdown is not a substitute for those encodings. Lean proofs are not the specification. spec_check remains form. Meaning model tests are checks.formal_vibefication_tests (Lake executable formal_vibefication_tests). Residual for this specification is Clause 6 of 0008_Formal_Vibefication.md.

7.12 Surmount Systems composition (not form rules)

Numbered specification 0010_Surmount_Systems.md is the contract that humans read for Surmount Systems stack composition. It is numbered specification 0010. Formal Vibefication is specification 0008. The word catalog is owned by CATE as specification 0005. Number 0009 is withdrawn. Companion Lean under lean/Surmount.lean composes human markdown, Lean spec encodings, Lean proofs, and product implementation: this specification as number 0010 with file name 0010_Surmount_Systems.md, unique numbers, CATE is 0005, RSI is 0006, CI is 0007, Formal Vibefication is 0008, vocabulary ownership is 0005, SSSSS is 0004, beastdb is 0003, Systems Lean is 0002, fargo unassigned, SSSP unspecified, leftover unstack nonconforming, byte identity required and not claimed true, products ongoing and not ready for use, this repository keeps spec encodings distinct from proofs and from markdown form (thisRepoSeparates), and Systems Lean product trees may unify those three (productTreeUnifies). Both facts can be true because they name different homes. Treating them as the same layer is inconsistent. Unification in a product tree is not a license to mix encodings with proofs here or to mix theorems into numbered markdown in this specifications repository. The Keagan backlink rule exists (proofofkeags.com when a numbered specification names Keagan or proofofkeags). If two models disagree on a number, that mash is a type error or False. Do not hide the disagreement behind a Bool.

That split follows lessons from Formal Vibefication and Taking Don't Trust. Verify. Seriously (accessed: 2026-08-25): theorems cover exactly what they state. This is not a copy of those papers.

Those modules are meaning proofs. They do not replace the markdown spec. They do not prove that Slake emit already matches ELF. They do not prove that beastdb, SSSSS, Slake, or Continuous Integration are ready for use. Meaning model tests are checks.surmount_tests (Lake executable surmount_tests). Residual for this specification is Clause 6 of 0010_Surmount_Systems.md.

7.13 Sibling line encodings (not form rules)

Formal Vibefication as specified in 0008_Formal_Vibefication.md requires every published numbered markdown file NNNN_descriptive_name.md at this repository root to have a sibling Lean spec encoding Spec_NNNN.lean at that same root. Lean module names cannot start with a digit. The Spec_ prefix exists so the module name is valid. Every physical line of the markdown, including blank lines, is an explicit Lean MdLine or String literal (line numbers that start at 1, exact text, optional role). include_str is not a line encoding. Encoded text matches the file bytes' lines (LF). Proofs of those encodings live in lean/Proofs_NNNN.lean, not in the sibling encoding file. A mash of encodings and their proofs in one file does not conform.

The durable checker is the Lean program line_encodings_check (library lean/LineEncodings.lean, shared type lean/MdLine.lean). It compares compiled encodedLines from each Spec_NNNN.lean to the markdown on disk. It fails when a markdown line has no encoding or an encoding has no matching markdown line. It also fails when that sibling contains include_str. The encoding is explicit Lean MdLine or String literals, one per physical markdown line. include_str is not a line encoding. Compiled encodedLines still must match the markdown bytes (LF lines). It fails when compiled encodedLines contain leftover unstack phrases in prose outside fenced code and inline code, and when comments in lean/FormalVibeficationSpec.lean or lean/VocabularySpec.lean contain those leftover phrases, using Cate.leftoverUnstackPhrases and the same leftover unstack scan as spec_check. That leftover unstack check is a floor, not a complete English checker, and it does not claim that every Lean comment is a complete American English thought. Hermetic fixtures are checks.line_encodings_tests. The repository scan is checks.line_encodings_check with REPO_ROOT set, the same pattern as vocab_aspell_tests. spec_check still discovers only NNNN_*.md. Spec_NNNN.lean is not a numbered specification.

The /lean4 prove cycle (Plan, Work, Checkpoint, Review) applies when writing or repairing those Lean modules. The /rsi skill is the factory for this checker: a later session runs line_encodings_check rather than a disposable job. Do not use include_str of the sibling markdown as a stand-in for those line encodings.

Meaning models such as lean/BeastDb.lean still mix encodings and proofs. That mash is remaining work under 0008. Sibling line encodings do not split those files.

7.14 Unique English word tracking (not form rules)

Numbered specification 0005_CATE.md owns the catalog of domain words. Root VOCABULARY.md is a pointer. The Lean program word_stats (library lean/WordStats.lean) lists unique English words in Surmount authored markdown at this repository root: numbered NNNN_*.md files, README.md, AGENTS.md, RESIDUAL.md, and VOCABULARY.md. Tokens are ASCII letters only, folded to lowercase. Digits are not words. beastdb is one token. RFC folds to rfc. Proven tokens are those CATE L_n catalog entries, plus RFC 2119 requirement keywords already named in 0000_spec.md Clause 4.1. That is not a second CATE catalog. Root WORD_STATS.md is the human report. The flake check fails when that report is stale. word_stats --write refreshes it.

This tracking is not a proof that every English sentence is CATE. The leftover unstack floor in 0005_CATE.md remains a separate check. Lean comments are not in the scan. Vendor trees under ref/, the Lean 4 skill pack, Lake build output, Nix result links, and git metadata are not in the scan. Hermetic fixtures are checks.word_stats_tests. The repository scan is checks.word_stats with REPO_ROOT set.

The /rsi skill is the factory for this checker: a later session runs word_stats rather than a disposable job.

8. Development shell and pre-commit

This project uses a Nix flake so that a pre-commit hook can run the Lean validator when you commit on a machine with the development shell installed.

1. Enter the shell (installs the repository pre-commit hook via the flake shell hook):

nix develop "path:$PWD"
# or: just dev

2. Optionally run hooks on every file without committing:

nix develop "path:$PWD" -c pre-commit run --all-files

3. Tools on the shell PATH include just, lean / lake (nixpkgs lean4), spec_check, aspell via aspellWithDicts (en_US) for local ad hoc use, and git. Spelling and whitespace across the project are flake checks, not shell package aliases. Use nix flake check for the full gate, or nix eval "path:$PWD#lib.whitespaceViolations" to debug whitespace.

The pre-commit Lean hook matches only numbered specifications (^[0-9]{4}_[A-Za-z0-9_]+\.md$), so README, AGENTS, and UNLICENSE are not subject to full RFC 2119 / style rules unless you pass them to spec_check explicitly. Whitespace across the project is enforced by pure Nix checks.whitespace on nix flake check, not by a bash pre-commit hook.

.pre-commit-config.yaml is generated by git-hooks.nix when you enter nix develop (it is typically a store symlink, not a hand maintained source file). Do not hand edit that file; change hook definitions in flake.nix and reenter the development shell so the generated config refreshes. Prefer the flake and this README over hard coding third party hook product names as process law.

9. Residual

Remaining work for the numbered specification program is written in full in RESIDUAL.md. Clause 6 of 0003_beastdb.md is the residual record for that specification. Clause 6 of 0004_SSSSS.md is the residual record for SSSSS. Clause 6 of 0005_CATE.md is the residual record for CATE. Clause 6 of 0006_RSI.md is the residual record for Recursive Self Improvement. Clause 6 of 0007_CI.md is the residual record for Continuous Integration and stack consistency. Clause 6 of 0008_Formal_Vibefication.md is the residual record for Formal Vibefication. Clause 6 of 0005_CATE.md also records that number 0009 is withdrawn and that the word catalog lives in CATE. Clause 6 of 0010_Surmount_Systems.md is the residual record for Surmount Systems stack composition. A parenthetical planned file name in Scope is not enough by itself.

Do not create 0005_fargo.md. Number 0005 is CATE. Number 0006 is Recursive Self Improvement. Do not invent a number for fargo. Do not create a numbered specification for Carbonado unless the operator asks. Number 0006 is RSI, not Carbonado. Number 0007 is Continuous Integration. Number 0008 is Formal Vibefication. Number 0009 is withdrawn. Do not create 0009_VOCABULARY.md. Number 0010 is Surmount Systems. Do not assign 0009 to fargo or Carbonado. beastdb, SSSSS, Slake, and Continuous Integration are ongoing and not ready for use. Do not write that they never started or do not exist. Do not claim Slake emit already matches object files as identical bytes. Numbered specification 0010_Surmount_Systems.md is the human contract for stack composition. lean/Surmount.lean is a model of composition of those identities. It is not a proof that Slake emit already matches ELF or that beastdb is ready for use. Every published numbered markdown file has a sibling Spec_NNNN.lean and a proof module lean/Proofs_NNNN.lean. Companion models other than the Formal Vibefication pair and the Vocabulary pair still mix encodings and proofs; that mash is remaining work. Lean Machine has no numbered specification. SSSP is not specified. ISO 24495-1:2023 and the US Federal Plain Language Guidelines are not pinned under ref/. CATE does not replace RFC 2119. CATE is specification 0005. The Systems Lean product tree that already holds Lean 4, CompCert, Idris 2, and Rust as git submodules is /home/hunter/Projects/ai/iso. Do not copy those four trees into this repository's ref/. The unsigned commit exception in 0007_CI.md is unique and is not claimed by this specifications repository.

10. Project skill /surmount-specify

Grok Build encodes numbered specifications in this repository with the project skill at .agents/skills/surmount-specify/SKILL.md. Run /surmount-specify when pasting a spec draft or adding a numbered specification. The skill is this repository only. Project skills live under .agents/skills/, not ~/.grok and not .grok/skills/. It does not replace 0000_spec.md. It tells the agent to read 0005_CATE.md, keep numbered markdown as the human contract, encode the specification in Lean, keep proofs in separate Lean modules, add a sibling Spec_NNNN.lean at the repository root whose physical lines match the markdown, keep those proofs in lean/Proofs_NNNN.lean, update lean/SpecRegistry.lean, write residual in full, and run nix flake check "path:$PWD" --print-build-logs. Stack numbers include published 0007_CI.md, published 0008_Formal_Vibefication.md, withdrawn 0009, and published 0010_Surmount_Systems.md. The word catalog lives in 0005_CATE.md. Tests that every published file is present use publishedBasenames.

11. Project skill /rsi

Grok Build builds durable engineering tools in this repository with the project skill at .agents/skills/rsi/SKILL.md. Run /rsi when adding a Lean checker, a Nix check, a project skill, or a helper used next to a compiler that a later session can run. The skill is this repository only. Project skills live under .agents/skills/, not ~/.grok and not .grok/skills/. It does not replace 0006_RSI.md. It tells the agent to follow Recursive Self Improvement and Concise American Technical English (0005_CATE.md): prefer a durable tool over a disposable job, use the large language model as a tool factory, pick the best available tool that can state the theorem, observe a failing test first, write residual in full, and run independent streams as parallel tightly scoped agents. When the durable tool is Lean, follow .agents/skills/lean4/SKILL.md. The line encoding checker line_encodings_check is one such tool. The word tracking checker word_stats is another. Number 0007 is Continuous Integration (0007_CI.md); do not steal 0007 for fargo.

12. Project skill /lean4

Grok Build proves companion Lean meaning models in this repository with the project skill at .agents/skills/lean4/SKILL.md. Run /lean4 when writing or repairing lean/*.lean. The wrapper is a real file, not a symlink. It tells the agent to read the pack at skills/lean4-skills/plugins/lean4/skills/lean4/SKILL.md and to use that pack as Plan, then Work (prove or autoprove), then Checkpoint, then Review, then golf. Formal Vibefication (0008_Formal_Vibefication.md) stays: numbered specification markdown is the contract humans read; the specification is also encoded in Lean as declarations of what must be true; proofs live in separate Lean modules; Lean proofs are not the specification. The prove cycle is Plan, then Work (prove or autoprove), then Checkpoint, then Review, then golf. Every published numbered markdown file has a sibling Spec_NNNN.lean; proofs of those line encodings live in lean/Proofs_NNNN.lean. Theorems cover exactly what they state. Lessons from Formal Vibefication and Taking Don't Trust. Verify. Seriously (accessed: 2026-08-25); this is not a copy of those papers. In product trees, Systems Lean (0002) and SSSSS (0004) may unify spec, proof, and implementation. That unification is not a license to mix spec encodings with proofs in this specifications repository, and is not a license to mix theorems into numbered markdown here. Numbered specification 0010_Surmount_Systems.md is the human contract. The composition proof is lean/Surmount.lean (surmountSpecNumber = 10, formalVibeficationSpecNumber = 8, vocabularySpecNumber = 9, Lake executable surmount_tests, flake check surmount_tests). Spec encodings for 0008 are lean/FormalVibeficationSpec.lean. Proofs are lean/FormalVibeficationProofs.lean (Lake executable formal_vibefication_tests). Spec encodings for 0009 are lean/VocabularySpec.lean. Proofs are lean/VocabularyProofs.lean. This Lake package has no mathlib. Do not add mathlib. The constructor for multiplicity omega is unrestricted (not omega). No sorry in shipped theorems. The gate is nix flake check "path:$PWD" --print-build-logs, not lake build alone. Never git commit from the skill. Do not set the nested plugin tree as the only skill discovery root. Populate the submodule with git submodule update --init skills/lean4-skills.

13. License

This work is released into the public domain under the Unlicense. See UNLICENSE.md. SPDX license identifier: Unlicense. The Lean 4 agent skill pack at skills/lean4-skills remains original work under the MIT license. This repository's Unlicense does not relicense that pack.