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.

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, 0009_PDOSS.md, 0010_Surmount_Systems.md, 0011_Surmount_Systems_Tech_Tree.md, 0012_Majestic_Memex.md, 0013_Lean_Machine.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 Public Domain Open Source Software (PDOSS). Unlicense remains the license. The file 0009_VOCABULARY.md MUST NOT exist. Number 0011 is Surmount Systems Tech Tree. The file 0011_Unlicense.md MUST NOT exist. Number 0012 is Majestic Memex. Number 0013 is Lean Machine. 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

0000_spec.md - Surmount spec spec (spec 0), version 0.1.0. Defines how specs in this repository are written, named, versioned, cited, and checked. Clause 11.4 requires markdown path links that reference material in this repository to resolve to a path that exists, checked by Lean repo_links_check. 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 0.1.0 by operator order. Changelog history records that a 1.4.0 line existed.
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/.
0002_Systems_Lean.md - Systems Lean, version 0.1.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 encodings live under lean/SystemsLeanSpec.lean. Proofs live under lean/SystemsLeanProofs.lean. Those modules are not the numbered specification. The Smart Symbolic Supercompiler is specified in 0004_SSSSS.md, including application and neurosymbolic integration. Lean Machine is specified in 0013_Lean_Machine.md. beastdb is specified in 0003_beastdb.md.
0003_beastdb.md - beastdb, version 0.1.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 encodings live under lean/BeastDbSpec.lean. Proofs live under lean/BeastDbProofs.lean. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
0004_SSSSS.md - Surmount Systems Smart Symbolic Supercompiler, version 0.1.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; specifies neurosymbolic integration when a product claims that harness interface (symbolic interface in Systems Lean, neural path only when that interface cannot complete the action, tool improvements reduced to sequential integers, training a model not a substitute for tool improvement inside the harness). That integration is specified and is not a shipped product. Lean Machine is specified in 0013_Lean_Machine.md. This specification does not claim a conforming implementation exists. Companion Lean meaning encodings live under lean/SssssSpec.lean. Proofs live under lean/SssssProofs.lean. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
0005_CATE.md - Concise American Technical English, version 0.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. The operator later assigned 0009 to Unlicense, then to Public Domain Open Source Software (PDOSS) (0009_PDOSS.md) to fill that gap. Unlicense remains the license. The file 0009_VOCABULARY.md MUST NOT exist. Number 0011 is Surmount Systems Tech Tree. 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 encodings live under lean/CateSpec.lean. Proofs live under lean/CateProofs.lean. Catalog encodings live under lean/VocabularySpec.lean. Proofs of that catalog 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.
0006_RSI.md - Recursive Self Improvement, version 0.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 encodings live under lean/RsiSpec.lean and lean/Vocabulary.lean. Proofs live under lean/RsiProofs.lean and lean/VocabularyCollisionProofs.lean. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
0007_CI.md - Continuous Integration and stack consistency, version 0.1.0. Requires the named gate green before commit and before push (this repository's gates are just check-local on this laptop and just check-remote on the remote builder host named surmount-1), 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 encodings live under lean/CiSpec.lean. Proofs live under lean/CiProofs.lean. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
0008_Formal_Vibefication.md - Formal Vibefication, version 0.1.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 NNNN_descriptive_name.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 Public Domain Open Source Software (PDOSS) (0009_PDOSS.md). Unlicense remains the license. The word catalog lives in CATE (0005_CATE.md). The file 0009_VOCABULARY.md MUST NOT exist. Number 0011 is Surmount Systems Tech Tree. 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.
0009_PDOSS.md - Public Domain Open Source Software (PDOSS), version 0.1.0. Defines the PDOSS test as a public domain dedication of software that is open. Records that Unlicense meets that test and remains the license (UNLICENSE.md). Records that MIT as used by the Lean 4 agent skill pack and Apache 2.0 as used by the btc-verified pin do not meet a public domain dedication test. Records that a mash that claims MIT meets PDOSS is False. Requires numbered specifications and the Lean in this tree to be dedicated to the public domain under the Unlicense except where residual names a different license. Records that ideas are not scarce and that two people can hold the same idea at once. The Lean 4 agent skill pack remains MIT. Essays by Keagan McLelland (Proof of Keags) are not Unlicense; citations keep canonical URLs on https://proofofkeags.com . Refusing a tool the author cannot improve is RSI process residual, not a claim that every product is Unlicense. Formal Vibefication split: encodings in lean/UnlicenseSpec.lean, proofs in lean/UnlicenseProofs.lean, sibling 0009_PDOSS.lean. A mash of spec encodings and their proofs is False. Number 0009 was briefly Vocabulary, then Unlicense, and is now PDOSS by operator order. The Unlicense numbered markdown file for specification 0009 MUST NOT exist. The file 0009_VOCABULARY.md MUST NOT exist. Number 0011 is Surmount Systems Tech Tree. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
0010_Surmount_Systems.md - Surmount Systems, version 0.1.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 NNNN_descriptive_name.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 Public Domain Open Source Software (PDOSS) (0009_PDOSS.md). Unlicense remains the license. The word catalog lives in CATE (0005_CATE.md). The file 0009_VOCABULARY.md MUST NOT exist. Number 0011 is Surmount Systems Tech Tree (0011_Surmount_Systems_Tech_Tree.md). fargo, SSSP, and Carbonado remain unspecified. Lean Machine is specified in 0013_Lean_Machine.md. 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.
0011_Surmount_Systems_Tech_Tree.md - Surmount Systems Tech Tree, version 0.1.0. Directed acyclic graph of relationships among numbered specifications, sibling Lean encodings, materials under ref/, SOURCE.md, skills, and other cited files, for lookup in the style of a memex. Specifies the .sstt binary format with magic SSTECHTREE01 and Bitcoin canonical CompactSize counts. The encoded graph MUST be a directed acyclic graph. Markdown citation among numbered specifications MAY cycle. This Lake package includes a Lean writer and reader of .sstt files (lean/Sstt.lean, command sstt_write). That writer is not a shipped memex product. CompactSize full UInt64 proof remains in btc-verified. The Form 1 pin is ref/btc-verified. Markdown path links in this repository are checked by repo_links_check. Number 0012 is Majestic Memex (0012_Majestic_Memex.md). Formal Vibefication split: encodings in lean/TechTreeSpec.lean, proofs in lean/TechTreeProofs.lean, sibling 0011_Surmount_Systems_Tech_Tree.lean. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
0012_Majestic_Memex.md - Majestic Memex, version 0.1.0. Human contract for crate majestic, command memex, on disk magic MAJESTIC plus byte 0x01, extension .majestic, and data under $HOME/memex. This format is not Tech Tree .sstt. A memex product MAY later load a .sstt file. The crate at ~/majestic is version 0.1 and still being built. It is not ready for use. The Unlicense of this specifications repository does not silently cover that crate. Formal Vibefication split: encodings in lean/MemexSpec.lean, proofs in lean/MemexProofs.lean, sibling 0012_Majestic_Memex.lean. Residual for this specification is Clause 6 of that file; residual for the numbered specification program is RESIDUAL.md.
0013_Lean_Machine.md - Lean Machine, version 0.1.0. Human contract for Systems Lean, Legal Lean, and Holy Lean as one symbolic proof machine. Important work is Unlicense as specified in 0009_PDOSS.md. The Systems Lean component follows 0002_Systems_Lean.md with CompCert ccomp and a bootstrapped Slake that fully typechecks REQUIRED for that named high assurance path. Legal Lean and Holy Lean are named components without separate stack numbers and are not done. The machine MUST attempt deterministic answers and MUST timestamp a note when an answer is wrong or imprecise. Distributed self improvement is a design requirement citing 0006_RSI.md, not a claim that the machine already runs. Worship and belief are not conformance conjuncts. This specification does not claim a conforming Lean Machine exists. Formal Vibefication split: encodings in lean/LeanMachineSpec.lean, proofs in lean/LeanMachineProofs.lean, sibling 0013_Lean_Machine.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 Public Domain Open Source Software (PDOSS) (0009_PDOSS.md). Unlicense remains the license. The file 0009_VOCABULARY.md MUST NOT exist. Number 0011 is Surmount Systems Tech Tree. Number 0012 is Majestic Memex. Number 0013 is Lean Machine.

3. Document rules

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

American English spelling and wording throughout (en_US).
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.
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.
Enumerate sections and lists clearly. Use numbered or lettered lists. Do not use markdown bullet markers (-, *, +) outside fenced code.
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.
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.
Maintain high precision. Label open questions and behavior the implementation defines. Do not leave silent gaps implementers need filled.
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).
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.
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").
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

Specs use real Semantic Versioning (SemVer) 2.0.0: MAJOR.MINOR.PATCH. Cite SemVer; local copy path when present: ref/semver.
The repository operator controls when a specification is published.
By operator order, numbered specifications other than 0001_DOGE.md carry version line 0.1.0. Digital Octal Graphical Emissive (DOGE) remains 1.0.0. Do not require first publication 1.0.0 for those files. Changelog history MAY record that a 1.0.0 line existed. That 0.1.0 line is the current version on disk. It is not a fake history of shipped 0.x releases.
Specs MAY carry a SemVer version line (see the pattern in 0000). A version line 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.
After publication, incompatible changes raise MAJOR; backward compatible additions raise MINOR; compatible fixes raise PATCH, as SemVer describes.
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.md (Form 2) or sibling .SOURCE (Form 1) 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.

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.md 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.
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.
Adding a new external citation in a spec requires adding or updating the matching ref/ entry under that process.
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.md. 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.md 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.md. Ecma text copyright policy allows unchanged republication with notice. Community reformats are not the Ecma publisher source. See ref/ecma48/SOURCE.md 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.md. No canonical git that the publisher maintains. Surmount does not own the text. See ref/itu_t416/SOURCE.md and ref/README.md.
Paths may be documented before the directories are populated. Empty paths are not an excuse to drop the public citation.
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.
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.

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.

Run the full Nix flake check on this laptop with just check-local. That recipe keeps builds on this machine and does not send work to the remote builder host named surmount-1.

Run the full Nix flake check on the remote builder host named surmount-1 with just check-remote. That recipe uses this machine's configured remote Nix builder. It fails if that builder cannot start.

just check is the same Nix flake check and follows this machine's Nix config, which may send builds to a remote builder. You do not need just if you invoke Nix yourself. The just recipes pass this repository as a Nix flake path so untracked flake files still evaluate. CI installs Nix and runs the flake check after checkout (workflow: .github/workflows/check.yml). CI does not install or invoke just. Checkout initializes Form 1 git submodules. Form 2 pins need no submodule init.

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):

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, 0009_PDOSS.md, and 0010_Surmount_Systems.md; a stale 0005_fargo.md token must fail; a stale 0011_Unlicense.md token must fail; withdrawn 0009_VOCABULARY.md must fail; withdrawn Unlicense numbered markdown for specification 0009 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. Residual honesty also fails when numbered specifications or extra Surmount authored markdown (AGENTS.md, README.md, RESIDUAL.md, VOCABULARY.md) assert that a named product does not exist as if it never started. The honesty BAN that says authors MUST NOT write that a product never started or does not exist is allowed. 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.
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.
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.
checks.spec_check_tests - hermetic Lean unit tests for spec_check form rule helpers (string fixtures).
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.
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.
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.
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.
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.
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.
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 Public Domain Open Source Software (PDOSS); Unlicense remains the license; 0009_VOCABULARY.md MUST NOT exist. Number 0011 is Surmount Systems Tech Tree.
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; a fixture with tests and no model does not conform; a complete science cycle conforms; number 0008 is published; number 0009 is Public Domain Open Source Software (PDOSS); number 0011 is Surmount Systems Tech Tree. This is not a second markdown form checker.
checks.unlicense_tests - spec encodings and separate proofs for PDOSS as specification 0009 (lean/UnlicenseSpec.lean and lean/UnlicenseProofs.lean): PDOSS test; Unlicense meets that test; MIT and Apache 2.0 do not meet a public domain dedication test; mash MIT-meets-PDOSS is False; remaining copyright on a grant that keeps copyright; Unlicense dedication has no remaining copyright in the model; ideas are not scarce; this repository Unlicense except named residual licenses; a mashed module that holds encodings and their proofs does not conform. Lake keeps the UnlicenseSpec library name. Unlicense remains the license. This is not a second markdown form checker.
checks.tech_tree_tests - spec encodings and separate proofs for Surmount Systems Tech Tree as specification 0011 (lean/TechTreeSpec.lean and lean/TechTreeProofs.lean): magic SSTECHTREE01; CompactSize golden vectors; DAG fixtures; a mashed module that holds encodings and their proofs does not conform. This is not a second markdown form checker.
checks.memex_tests - spec encodings and separate proofs for Majestic Memex as specification 0012 (lean/MemexSpec.lean and lean/MemexProofs.lean): crate majestic; command memex; magic MAJESTIC plus byte 0x01; extension .majestic; data under $HOME/memex; distinct from Tech Tree .sstt; the crate is still being built; this repository Unlicense does not silently cover ~/majestic; a mashed module that holds encodings and their proofs does not conform. This is not a second markdown form checker.
checks.lean_machine_tests - spec encodings and separate proofs for Lean Machine as specification 0013 (lean/LeanMachineSpec.lean and lean/LeanMachineProofs.lean): assignment as number 0013; Unlicense of important work as specification 0009; Systems Lean as specification 0002 with CompCert and a bootstrapped Slake that fully typechecks required; Legal Lean and Holy Lean as named components without separate numbers; timestamped notes; deterministic answers; distributed self improvement as a design requirement; worship not required for conformance; a mashed module that holds encodings and their proofs does not conform. This is not a second markdown form checker.
checks.sstt_tests - Lean writer and reader of .sstt files (lean/Sstt.lean): wrong magic is rejected; a DAG roundtrip matches; a cyclic encoded graph fails; when two numbered specifications mention each other the encoded edge goes from the lower spec number to the higher; withdrawn names 0009_VOCABULARY.md, 0005_fargo.md, and 0011_Unlicense.md are not nodes; published numbered specification nodes match the registry, including 0012_Majestic_Memex.md; the writer refuses to write tech_tree.sstt into the repository root; when REPO_ROOT is this repository, --decode of a graph that is missing a published numbered specification fails; without REPO_ROOT, --decode of that same kind of graph, or of a small valid graph that is not this tree, does not require the published numbered specification set; a cited skill, ref/ pin, or SOURCE dest missing from the file list fails honesty; a present dest still writes a DAG and classifies the node; remote http:// dests do not fail this writer check. The command sstt_write writes a .sstt file from this repository. With no -o, it writes tech_tree.sstt under a new temporary directory. Pass -o for any other path. Run sstt_write with REPO_ROOT set to this repository root so the writer finds the specs. This is not Majestic Memex and is not a second markdown form checker.
checks.repo_links_tests - hermetic fixtures for markdown path links: a missing path target fails; http:// and https:// are skipped; fragment only targets are the same file.
checks.repo_links_check - markdown [text](target) path links in numbered specifications and README.md resolve to an existing path. Skip http:// and https://. This floor does not parse every HTML href.
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, PDOSS is 0009, the word catalog is owned by CATE as 0005, number 0011 is Surmount Systems Tech Tree, 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 NNNN_descriptive_name.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.
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.
checks.line_encodings_check - Lean program line_encodings_check reads each root NNNN_*.md and the compiled lines from sibling NNNN_descriptive_name.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, lean/VocabularySpec.lean, lean/Vocabulary.lean, lean/TechTreeSpec.lean, lean/MemexSpec.lean, lean/UnlicenseSpec.lean, lean/CateSpec.lean, lean/RsiSpec.lean, lean/CiSpec.lean, the beastdb meaning spec encoding under lean/, lean/SssssSpec.lean, lean/SystemsLeanSpec.lean, and lean/LeanMachineSpec.lean contain those leftover phrases, using Cate.leftoverUnstackPhrases and the same leftover unstack scan as spec_check. It also fails when compiled encodedLines or those same comments contain never-real product claims, using SpecCheck.neverRealProductPhrases and the same residual honesty 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; NNNN_descriptive_name.lean is not a numbered specification. This is not a second markdown form checker.
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.
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.
checks.inconsistency_report_tests - hermetic Lean unit tests for the README table of proven logical inconsistency in Lean meaning models: a missing table fails; a stale table versus proven False mash claims fails; a matching table passes. This is not a second markdown form checker.
checks.inconsistency_report - Lean program inconsistency_report fails when README.md is missing the marked table of proven logical inconsistency in this repository's Lean meaning models, or when that table is stale versus the catalog in lean/InconsistencyReport.lean. Thin runCommand sets REPO_ROOT and runs the binary. inconsistency_report --write refreshes the marked table. Reasoning for listed claims lives in RESIDUAL.md. Agents are not the glue. This is not a second markdown form checker.
checks.sstt_write - Lean program sstt_write --self-check writes a .sstt file from this repository into the Nix check output (not the repository root), reads it back, and fails on wrong magic, a cyclic encoded graph, a missing published numbered specification node, a withdrawn name as a node, or a cited skill, ref/ pin, or SOURCE dest missing from disk. A present dest still writes a DAG and classifies the node. Remote http:// dests do not fail this writer check. Thin runCommand sets REPO_ROOT to this repository and runs sstt_write --self-check -o "$out/tech_tree.sstt". When REPO_ROOT is this repository, sstt_write --decode applies the same published numbered specification set check. Without REPO_ROOT, --decode of an arbitrary file does not. This is not a shipped Surmount product writer and is not a second markdown form checker.

Numbered specifications matched for Lean and spelling:

Glob at repository root: [0-9][0-9][0-9][0-9]_*.md
Basename regex: ^[0-9]{4}_[A-Za-z0-9_]+\.md$
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, 0009_PDOSS.md, 0010_Surmount_Systems.md, 0011_Surmount_Systems_Tech_Tree.md
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 (spec_check_tests, systems_lean_tests, beastdb_tests, sssss_tests, cate_tests, rsi_tests, ci_tests, vocab_aspell_tests, formal_vibefication_tests, unlicense_tests, surmount_tests, line_encodings_tests, word_stats_tests, inconsistency_report_tests) 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.md 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:

Pure ASCII (tab, LF, printable 0x20-0x7E; no CR or high bytes).
No markdown bullet list markers (-, *, +) outside fenced code.
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.
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).
No trailing whitespace (space or tab before end of line).
No leading indent with spaces (use tabs for nested markdown indent).
No prose wrapped to a column on numbered specifications (heuristic outside fences and tables; see 0000_spec.md Clause 6.4).
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.
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.
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.
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.
Residual honesty: do not assert that a named product never started by writing that a conforming product does not exist. Scans numbered specifications plus AGENTS.md, README.md, RESIDUAL.md, and VOCABULARY.md. The honesty BAN that says authors MUST NOT write that a product never started or does not exist is allowed. A numbered Vocabulary file MUST NOT exist is allowed. Path link checks are allowed.

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

Same trailing whitespace and leading space rules on Surmount authored text (*.md, *.nix, SOURCE.md pins we write, leftover SOURCE if present, and similar).
Skips vendor material: ref/semver/**, *.pdf, ref/**/rfc2119.txt.
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.
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:

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

How to fix:

Join each paragraph (and each list item body) into one physical line. Let the editor soft wrap.
Keep deliberate structure breaks: blank lines between paragraphs, one list item per line, headings, fences, tables.
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

The rule set is small (trailing space/tab; leading space ban with known exemptions).
Implementation needs only fileset discovery, readFile, and line scans.
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

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

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.
Do not move whitespace across the tree into Lean only for symmetry with form rules.
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 0009_PDOSS.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 unlicense_tests
./.lake/build/bin/unlicense_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

The gates the operator uses are just check-local and just check-remote, as named in 7.1. Those recipes invoke Nix flake check. CI runs that same flake check after installing Nix.

just check
just check-local
just check-remote

If you invoke Nix without just, use this repository as a flake path so untracked flake files still evaluate. The Lean form checker package is spec_check. Individual flake checks use the current system name.

Flake layout:

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, unlicense_tests, tech_tree_tests, memex_tests, lean_machine_tests, sstt_tests, repo_links_tests, line_encodings_tests, word_stats_tests, and inconsistency_report_tests, plus the line encoding checker line_encodings_check, the markdown path link checker repo_links_check, the word tracking checker word_stats, the proven inconsistency table checker inconsistency_report, and the .sstt writer sstt_write.
apps: only spec_check (also default -> same binary path).
checks: spec_check (form rules + spelling + registry scan + CATE leftover unstack and residual heading + Keagan back linking + residual honesty that a named product is not asserted never started), 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), unlicense_tests (0009 spec encodings versus proofs, not form rules), tech_tree_tests (0011 spec encodings versus proofs, CompactSize golden vectors, not form rules), memex_tests (0012 spec encodings versus proofs, not form rules), lean_machine_tests (0013 spec encodings versus proofs, not form rules), sstt_tests (writer and reader of .sstt files, including --decode with and without REPO_ROOT, not form rules), sstt_write (write a .sstt file from this repository, read it back, fail on wrong magic or a missing published numbered specification; output is the Nix check store path, not the repository root), repo_links_tests (hermetic fixtures for markdown path links, not form rules), repo_links_check (markdown path links in numbered specifications and README resolve to existing paths), 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 NNNN_descriptive_name.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), inconsistency_report_tests (hermetic README table fixtures, not form rules), inconsistency_report (README table of proven False mash claims matches the Lean catalog; reasoning in RESIDUAL.md), whitespace, pre-commit-check (each independent; no bash orchestrated aggregate package).
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/SystemsLeanSpec.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/BeastDbSpec.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, 0009 PDOSS, 0010 Surmount Systems, 0011 Surmount Systems Tech Tree, 0012 Majestic Memex, 0013 Lean Machine). Planned rows are empty. Number 0011 is Surmount Systems Tech Tree. Number 0012 is Majestic Memex. Number 0013 is Lean Machine. The Lean field named published on those fourteen 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), PDOSS = 9, Surmount Systems = 10, Lean Machine = 13, fargo unassigned, SSSP unassigned, and Carbonado unassigned. Unlicense remains the license. The identifier unlicenseSpecNumber MAY remain 9 because Unlicense remains the license. 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 stale 0011_Unlicense.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/SssssSpec.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 is specified in 0013_Lean_Machine.md.

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/CateSpec.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/RsiSpec.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/CiSpec.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 Public Domain Open Source Software (PDOSS) (0009_PDOSS.md). Unlicense remains the license. The word catalog lives in CATE (0005_CATE.md). The file 0009_VOCABULARY.md MUST NOT exist. Number 0011 is Surmount Systems Tech Tree. 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 NNNN_descriptive_name.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 PDOSS spec encodings and proofs (not form rules)

Numbered specification 0009_PDOSS.md is the contract that humans read for Public Domain Open Source Software. It is numbered specification 0009. Unlicense remains the license. The Unlicense numbered markdown file for specification 0009 MUST NOT exist. The file 0009_VOCABULARY.md MUST NOT exist. Number 0011 is Surmount Systems Tech Tree. Lean spec encodings under lean/UnlicenseSpec.lean state what must be true: the PDOSS test; Unlicense meets that test; MIT and Apache 2.0 do not meet a public domain dedication test; a mash that claims MIT meets PDOSS is False; a grant that keeps copyright still has remaining copyright; an Unlicense dedication has no remaining copyright in the model; ideas are not scarce; two people can hold the same idea at once; numbered specifications and the Lean in this tree are Unlicense except named residual licenses; a mash of spec encodings and their proofs is False. Lake keeps the UnlicenseSpec library name. Lean proofs under lean/UnlicenseProofs.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. The Lean 4 agent skill pack remains MIT. Essays by Keagan McLelland (Proof of Keags) are not Unlicense. Numbered markdown is not a substitute for those encodings. Lean proofs are not the specification. spec_check remains form. Meaning model tests are checks.unlicense_tests (Lake executable unlicense_tests). Residual for this specification is Clause 6 of 0009_PDOSS.md.

7.13 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. Public Domain Open Source Software is specification 0009. Unlicense remains the license. The word catalog is owned by CATE as specification 0005. The file 0009_VOCABULARY.md MUST NOT exist. Number 0011 is Surmount Systems Tech Tree. 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, PDOSS is 0009, 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.14 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 NNNN_descriptive_name.lean at that same root. The encoding file uses the markdown basename with .lean in place of .md so a reader sees the pair immediately. The file name starts with a digit, so Lean uses a quoted module name that matches that stem. 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 NNNN_descriptive_name.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, lean/VocabularySpec.lean, lean/Vocabulary.lean, lean/TechTreeSpec.lean, lean/MemexSpec.lean, lean/UnlicenseSpec.lean, lean/CateSpec.lean, lean/RsiSpec.lean, lean/CiSpec.lean, the beastdb meaning spec encoding under lean/, lean/SssssSpec.lean, lean/SystemsLeanSpec.lean, and lean/LeanMachineSpec.lean contain those leftover phrases, using Cate.leftoverUnstackPhrases and the same leftover unstack scan as spec_check. It also fails when compiled encodedLines or those same comments contain never-real product claims, using SpecCheck.neverRealProductPhrases and the same residual honesty 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. NNNN_descriptive_name.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 place encodings in Spec modules and theorems in Proofs modules: lean/CateSpec.lean and lean/CateProofs.lean, lean/RsiSpec.lean and lean/RsiProofs.lean, lean/CiSpec.lean and lean/CiProofs.lean, lean/BeastDbSpec.lean and lean/BeastDbProofs.lean, lean/SssssSpec.lean and lean/SssssProofs.lean, lean/SystemsLeanSpec.lean and lean/SystemsLeanProofs.lean, lean/FormalVibeficationSpec.lean and lean/FormalVibeficationProofs.lean, lean/UnlicenseSpec.lean and lean/UnlicenseProofs.lean, lean/TechTreeSpec.lean and lean/TechTreeProofs.lean, lean/MemexSpec.lean and lean/MemexProofs.lean, lean/LeanMachineSpec.lean and lean/LeanMachineProofs.lean, lean/VocabularySpec.lean and lean/VocabularyProofs.lean. Mixing encodings and proofs in one mash is False under 0008. Sibling line encodings remain a separate split. Collision tags in lean/Vocabulary.lean are encodings with proofs in lean/VocabularyCollisionProofs.lean.

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

7.16 Proven logical inconsistency table

0000_spec.md Clause 17.1 item 8 requires this README to keep a current table of proven logical inconsistency in this repository's Lean meaning models. The Lean program inconsistency_report generates or checks the marked table. Reasoning lives in RESIDUAL.md. The listed claims are intentional nonconformance theorems (a mashed spec encoding plus proof is False). They are not a stack numbering bug. Formal Vibefication as specification 0008 also requires a science cycle: a hypothesis, a model, a theory, a proof, tests, and corollary experiments. Tests alone are not enough. Companion meaning models for CATE, RSI, Continuous Integration, beastdb, SSSSS, Systems Lean, Surmount Systems Tech Tree, Majestic Memex, Public Domain Open Source Software (PDOSS; Unlicense remains the license), Lean Machine, the CATE word catalog, and Vocabulary collision encodings reuse FormalVibeficationSpec.ScienceEffort and conformingScience. Tests without a model do not conform. A model and proofs without corollary experiments do not conform. Those facts are not new mash theorems. The table below still lists the same six mash claims. Products named in this program are real, incomplete, and not ready for use.

Exists	File	Claim	Kind
yes	`lean/FormalVibeficationProofs.lean`	`mash_spec_and_proof`	intentional nonconformance theorem
yes	`lean/FormalVibeficationProofs.lean`	`mash_homes_is_inconsistent`	intentional nonconformance theorem
yes	`lean/UnlicenseProofs.lean`	`mash_spec_and_proof`	intentional nonconformance theorem
yes	`lean/UnlicenseProofs.lean`	`mash_mit_meets_pdoss`	intentional nonconformance theorem
yes	`lean/UnlicenseProofs.lean`	`mash_apache_meets_pdoss`	intentional nonconformance theorem
yes	`lean/Surmount.lean`	`mash_layers_inconsistent`	intentional nonconformance theorem

Hermetic fixtures are checks.inconsistency_report_tests. The repository scan is checks.inconsistency_report with REPO_ROOT set. inconsistency_report --write refreshes the marked table.

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.

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

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

Optionally run hooks on every file without committing:

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

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 the word catalog lives in CATE and that number 0009 is Public Domain Open Source Software (PDOSS). Clause 6 of 0009_PDOSS.md is the residual record for Public Domain Open Source Software. 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 Public Domain Open Source Software (PDOSS). Unlicense remains the license. Do not create 0009_VOCABULARY.md. Number 0010 is Surmount Systems. Number 0011 is Surmount Systems Tech Tree. Do not create 0011_Unlicense.md. 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 NNNN_descriptive_name.lean and a proof module lean/Proofs_NNNN.lean. Companion models named in 7.14 place encodings in Spec modules and theorems in Proofs modules. Mixing encodings and proofs in one mash is remaining work only if a later module reintroduces theorems into a Spec file. Lean Machine is specified in 0013_Lean_Machine.md. 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 NNNN_descriptive_name.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 just check-local plus just check-remote. Stack numbers include published 0007_CI.md, published 0008_Formal_Vibefication.md, published 0009_PDOSS.md, and published 0010_Surmount_Systems.md. The file 0009_VOCABULARY.md MUST NOT exist. Number 0011 is Surmount Systems Tech Tree. 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 NNNN_descriptive_name.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, unlicenseSpecNumber = 9, vocabularySpecNumber = 5, 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/UnlicenseSpec.lean. Proofs are lean/UnlicenseProofs.lean (Lake executable unlicense_tests). Spec encodings for the word catalog owned by CATE as 0005 are lean/VocabularySpec.lean. Proofs are lean/VocabularyProofs.lean. The file 0009_VOCABULARY.md MUST NOT exist. Number 0011 is Surmount Systems Tech Tree. 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 and numbered specification 0009_PDOSS.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. Essays by Keagan McLelland (Proof of Keags) are not Unlicense; citations keep canonical URLs on https://proofofkeags.com .

Name		Name	Last commit message	Last commit date
.agents/skills		.agents/skills
.github/workflows		.github/workflows
lean		lean
nix		nix
ref		ref
skills		skills
.gitignore		.gitignore
.gitmodules		.gitmodules
0000_spec.lean		0000_spec.lean
0000_spec.md		0000_spec.md
0001_DOGE.lean		0001_DOGE.lean
0001_DOGE.md		0001_DOGE.md
0002_Systems_Lean.lean		0002_Systems_Lean.lean
0002_Systems_Lean.md		0002_Systems_Lean.md
0003_beastdb.lean		0003_beastdb.lean
0003_beastdb.md		0003_beastdb.md
0004_SSSSS.lean		0004_SSSSS.lean
0004_SSSSS.md		0004_SSSSS.md
0005_CATE.lean		0005_CATE.lean
0005_CATE.md		0005_CATE.md
0006_RSI.lean		0006_RSI.lean
0006_RSI.md		0006_RSI.md
0007_CI.lean		0007_CI.lean
0007_CI.md		0007_CI.md
0008_Formal_Vibefication.lean		0008_Formal_Vibefication.lean
0008_Formal_Vibefication.md		0008_Formal_Vibefication.md
0009_PDOSS.lean		0009_PDOSS.lean
0009_PDOSS.md		0009_PDOSS.md
0010_Surmount_Systems.lean		0010_Surmount_Systems.lean
0010_Surmount_Systems.md		0010_Surmount_Systems.md
0011_Surmount_Systems_Tech_Tree.lean		0011_Surmount_Systems_Tech_Tree.lean
0011_Surmount_Systems_Tech_Tree.md		0011_Surmount_Systems_Tech_Tree.md
0012_Majestic_Memex.lean		0012_Majestic_Memex.lean
0012_Majestic_Memex.md		0012_Majestic_Memex.md
0013_Lean_Machine.lean		0013_Lean_Machine.lean
0013_Lean_Machine.md		0013_Lean_Machine.md
AGENTS.md		AGENTS.md
README.md		README.md
RESIDUAL.md		RESIDUAL.md
UNLICENSE.md		UNLICENSE.md
VOCABULARY.md		VOCABULARY.md
WORD_STATS.md		WORD_STATS.md
aspell_words.txt		aspell_words.txt
flake.lock		flake.lock
flake.nix		flake.nix
justfile		justfile

Uh oh!

Latest commit

History

Folders and files

Repository files navigation

Surmount miscellaneous specifications

Table of contents