From d4f8da315a96a53e42246de6599121b1faade197 Mon Sep 17 00:00:00 2001 From: Alberto Serrano-Calva Date: Sun, 9 Aug 2026 04:46:56 -0400 Subject: [PATCH 1/2] design(research-register): the palace adopts the literature's language without inflating its claims MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three mechanisms, one surfaced absence: a lexicon that teaches (alias and deepen, never replace — ids/commands/parsed strings frozen), a claim ladder that prices every label (agent ceiling: Proposition-with-checkable-proof; "Theorem" honest by absence), and the deskcheck evolved in place into an artifact-evaluation paper (same dc- lifecycle, board.py zero lines, book LaTeX factored not forked, PDFs to the exhaust lane never git). Plus the empty slot: the research Question, owner-only, surfaced not filled. Warrant: owner seed 2 in docs/brainstorms/mathematical-foundations.md (PR #42, sequenced first). Graduation licenses RR-1/2/3 on merge. --- docs/design-notes/dn-research-register.md | 777 ++++++++++++++++++++++ 1 file changed, 777 insertions(+) create mode 100644 docs/design-notes/dn-research-register.md diff --git a/docs/design-notes/dn-research-register.md b/docs/design-notes/dn-research-register.md new file mode 100644 index 0000000..a8b66b3 --- /dev/null +++ b/docs/design-notes/dn-research-register.md @@ -0,0 +1,777 @@ +--- +type: design-note +id: dn-research-register +track: workflow # the artifact chain's own register is how work moves; docs/tracks/workflow.md exists — no new manifest minted (its DoD gains rows, §3) +status: draft # provenance description, never a gate (merge-gated regime, 2026-07-28) +created: 2026-08-09 +updated: 2026-08-09 # revision pass, same day — four-audit verdicts applied +links: + - docs/brainstorms/mathematical-foundations.md # THE WARRANT (PR #42, capture branch — lands first; see Sequencing) — terminology seeds + the structure-instantiation bridge + - docs/design-notes/track-board-and-deskcheck-gate.md # RATIFIED parent — its D3 minted the deskcheck template/body this note evolves; D2's derived board is untouched + - docs/design-notes/external-grounding.md # RATIFIED — the verified-citation gate every paper bibliography obeys (never [FROM MEMORY]) + - docs/design-notes/erratum-relation.md # RATIFIED — correction = supersession composed with a warranted erratum; the retraction algebra the lexicon maps + - docs/design-notes/dn-typed-workflow-registry.md # RATIFIED (pre-regime) — parks deskcheck-verdict signing; that park is untouched here + - docs/design-notes/authorship-distance-axis.md # DRAFT at HEAD — agent-vs-owner authorship as a first-class coordinate; the provenance block leans on the idea + - docs/templates/deskcheck.md # the 17-line artifact re-typed here — evolved in place, never paralleled + - docs/book/preamble.tex # the house claim registry + citation macros the paper format factors and extends + - .claude/skills/book/SKILL.md # LaTeX conventions authority — reused, not forked + - .claude/skills/issue/SKILL.md # the label taxonomy the claim ladder maps onto +supersedes: null # PARTIAL overlay on dn-track-board-and-deskcheck-gate D3 — template/body shape only (§2.4); D3's pre-regime verdict-hook mechanics are not propagated; D2's board, the dc- lifecycle, and the queue are untouched +superseded_by: null +warrant: docs/brainstorms/mathematical-foundations.md # owner seed 2, 2026-08-09 — quoted in the opening blockquote; reaches main via PR #42, sequenced first +--- + +# The research register — the palace adopts the literature's language without inflating its claims + +> Composed at **fable** (`claude-fable-5`, xhigh, 2026-08-09; revision pass same day, +> same tier). Per the banner-unreliability lesson (finding-0147, frozen history: a +> composed-at banner is a claim, not a proof), the owner cross-checks usage at review. +> Agent-drafted, filed as `draft` on a branch. Under the merge-gated regime (owner +> ruling 2026-07-28) nobody flips a status — **the owner's merge of this PR is +> ratification**, and the `status:` line above is provenance description, never a gate. +> If this text is on `main`, the owner put it there. +> +> **Sequencing:** the warrant capsule lives only on the capture branch of PR #42 and is +> not at HEAD (verified: `git cat-file -e` fails at `68d8d39`). That PR lands first — +> or this branch stacks on it — so the warrant path resolves in the tree the reviewer +> reads. A note establishing citation hygiene does not itself merge with a dangling +> warrant. + +> *"capture-as-theorem gave me a thought: could/should we start using that terminology, +> and start adopting mathematical research style formats? we could refresh the templates +> and skills around framing and terminology that reflect the research community. this is +> also a little for me — I'd like to better understand mathematical/computer-science +> research language in research communities. it would add credibility, but more +> importantly it makes the project more accessible to the technical research communities. +> all this to also say: that's what a deskcheck could be — a research PDF document, typed +> in LaTeX, formatted like an academic/research paper, like an article in a math/science +> journal."* — owner, 2026-08-09. +> +> The answer, in one sentence: **adopt the register as an alias layer that teaches and a +> claim ladder that raises the bar — and evolve the deskcheck, in place, into the one +> genre it already is: an artifact-evaluation report, typed in the book's LaTeX.** + +## 1. Purpose and scope + +### 1.1 What this note decides + +Three mechanisms and one surfaced absence, presented as one note because they are one +move — the palace learning to say precisely what it knows, in the language of the +communities that invented the distinctions: + +1. **The lexicon** (§2.2) — a terminology layer mapping every house term to its + research-register counterpart, living in one glossary artifact (`docs/lexicon.md`), + loaded on demand, never resident in `CLAUDE.md`. Terms **alias and deepen; they never + replace** — the invariant is §2.1, and it is load-bearing. +2. **The claim ladder** (§2.3) — a rigor-honesty policy: which claim-strength labels + exist, what each one *costs*, and where labels attach. The register is adopted to + raise the bar, not to decorate; most of what the palace knows is conjecture and + proposition, and the ladder makes saying so the path of least resistance. +3. **The deskcheck as paper** (§2.4) — the deskcheck artifact evolves into a short + research paper: LaTeX, the book's conventions reused wholesale, the + artifact-evaluation genre, the same `dc-` lifecycle, the same board, the same owner + holding the same final say. Evolution of the existing artifact — the 2026-07-28 + regime just retired ceremony, and this note will not smuggle a new one in: the form + is chosen before a word is authored (§2.4.2), and the bill is priced in §3. +4. **The empty slot** (§2.6) — the research idiom sharpens what the palace has never + had: a stated research Question. This note surfaces the absence and builds the slot. + Authoring the Question is the owner's alone; not one word of it is drafted here. + +The track is `workflow` — the register governs how work is framed, recorded, and +evidenced, which is exactly what the workflow track already owns. No new manifest is +needed; `docs/tracks/workflow.md` exists at HEAD, and §3 licenses the working-material +DoD rows that make this work visible to the lane's own deskcheck. + +### 1.2 Non-goals (load-bearing — read at ratification) + +1. **No renaming of ids, commands, or machine-parsed strings.** `dn-`/`bp-`/`dc-` + grammars, the six slash commands, `type: track`, the `Build Plan — ` H1 prefix, the + `read-map` fence, the `## Follow-through` header, the intent-capsule caps, the commit + grammar — all frozen. The alias invariant (§2.1) is the positive form of this + non-goal. [ESTABLISHED — parser/vocabulary coupling verified at HEAD, §2.1's list.] +2. **No actual journal or venue submission.** No arXiv, no conference, no DOI minting. + The register is adopted internally; external publication is a parked decision with + the Question as its re-entry condition. [INFERENCE — the owner asked for + accessibility to research communities, not submission to them; parking the venue + keeps the smaller reading.] +3. **No retroactive rewriting of history.** Frozen surfaces (`docs/findings/**`, the + owner-questions inbox, sealed journals, merged notes and capsules) keep their + vocabulary byte-identical. The register applies forward. [ESTABLISHED — frozen + history is a standing rule.] +4. **`CLAUDE.md` gains nothing.** Not a glossary line, not a pointer. Depth lives in + the glossary and templates, loaded on demand. [ESTABLISHED — thinness rule.] +5. **The research Question is not authored here.** Study-not-product: the Question is + owner-only. This note builds the slot and leaves it empty, labeled empty. + [ESTABLISHED — owner-only authorship is a standing rule.] +6. **Lean / proof-assistant adoption stays parked.** Re-entry unchanged from the + warrant capsule: a claim a property test cannot falsify. Consequence for the ladder: + "Theorem" is expected to be rare-to-absent, and its absence is honest (§2.3). + [ESTABLISHED once the warrant lands — the capsule park, restated not reopened; the + capsule is this note's warrant and is sequenced first (PR #42, see Sequencing).] +7. **No second LaTeX stack.** The paper format factors the book's preamble and extends + its notation registry; it duplicates nothing. Two copies drift. [ESTABLISHED — DRY + is a defect, not a nit.] +8. **No new ritual.** The deskcheck's lifecycle, store, board parsing, and queue are + unchanged; the carrier `.md` alone remains a legal deskcheck, and the form is picked + before authoring, never waived after the cost is sunk (§2.4.2). If the paper ever + *delays* closure, the format has failed its own bar (falsifier F6). + [INFERENCE — "evolved, never paralleled" is this note's reading of the owner's seed + against the regime's retirement of ceremony; the owner confirms at ratification.] +9. **The laws-ledger sweep is not licensed here.** The per-component + claimed-structure + laws + falsifier sweep belongs to the sibling mathematical- + foundations arc (§1.3); this note only specifies the labels that sweep will consume. + [INFERENCE — sibling boundary drawn so neither arc balloons.] +10. **The dormant deskcheck-gate machinery is not retired here.** `gate-guard.sh`, + `_lib.py`'s verdict clauses, and `tests/integration/test_deskcheck_gate.py` stay + untouched; the carrier keeps their expected shape so they stay green. Disposition + is parked, and filed as a `parked` issue with this PR so it cannot silently rot. + [INFERENCE — a format change and a trust-boundary change never share a plan.] + +### 1.3 The sibling note — flagged, not resolved + +The warrant capsule carries two arcs. This note is the register arc. The foundations +arc — structure-instantiation as the bridge, the laws ledger, memberships first — +becomes **NEW NOTE — mathematical foundations and the laws ledger**, not yet written. +One shared boundary, flagged: the claim-ladder labels of §2.3 are *consumed* by the +laws ledger (each law lands as a labeled claim with a falsifier); neither note should +redefine the labels without the other. The float-epsilon caveat (float addition is +non-associative — the capsule's named foundational risk) appears in both: here as a +register rule (§2.3.3), there as substance. + +## 2. Principles / decision + +### 2.1 The invariant first: alias and deepen, never replace + +**Decision.** The research register is a *reading* of the house vocabulary, not a +rename of it. Every house term keeps its id grammar, its file paths, its commands, and +its machine-parsed strings; the research term is the teaching layer stacked on top. +Concretely: + +- `dc-NNN` never becomes `paper-NNN`; a capture is still `/capture`; a finding is still + an issue. The research term appears in prose, glossaries, templates' teaching + comments, and the paper genre — never in identifiers. +- **Vocabulary and parser move in the same PR or not at all** — and RR-1..3 (§3) move + no parser. The frozen machine layer, enumerated so review can grep for it: `type: + track` and the manifest keys (`scripts/board.py:143-155`), the `Build Plan — ` H1 + prefix (`board.py:160`), the ` ```read-map ` fence (`scripts/readmap.py:27`), the + verbatim `## Follow-through` header (checkpoint skill), the intent-capsule canonical + caps (`scripts/capsule.py:41,62`), the `type(scope): subject` commit grammar, and the + deskcheck front-matter schema (`board.py:283-294`). + +Why this is the right shape and not timidity: the house terms are *coordinates* — the +board, the queue, CI, and every merged artifact address by them. The research terms are +*meanings*. Coordinates must be stable; meanings are allowed to deepen. Breaking ids to +gain register would trade the system's addressability for its accent. + +### 2.2 The lexicon — one glossary that teaches + +**Where it lives.** `docs/lexicon.md` — a single authored artifact (not derived, not a +skill; there is no procedure to run, only meaning to load). Templates and the skills +that traffic in the mapped terms gain a one-line pointer (`Register: docs/lexicon.md`); +`CLAUDE.md` gains nothing. + +**The entry contract — four clauses, all mandatory, plus a mechanical fifth.** The +owner's stated goal is to *learn* the research language, so an entry that merely +renames is a defect. Every entry carries: (1) the **house meaning**, precise; (2) the +**research meaning** as the community actually uses it; (3) **why the mapping holds** — +the warrant for the analogy; (4) **where it breaks** — the disanalogy, stated plainly. +An analogy without its breaking point teaches wrong. The mechanical fifth clause is +**verification status**: a verified source with date, or `[FROM MEMORY]` — R6's +discipline applied to the glossary itself, so a reader always knows which glosses are +community practice recalled and which are checked. An optional sixth clause, **usage**, +says when the research term is admissible in house prose (rule of thumb: only where its +community meaning is fully earned; otherwise the house term stands). + +**The map — the index.** The glossary carries every row as a full entry per the +contract; this table is the index only (terse cells; the fourth clause — where each +mapping breaks — is prose, below). Every research-meaning gloss here is community +practice carried `[FROM MEMORY]` except where a verified source is named (§2.4.3's +badge definitions). + +| house term | research register | the mapping's warrant, one clause | +|---|---|---| +| capture / brainstorm capsule | **conjecture** | precise, falsifiable, believed, unproven — naming a sharp one is a contribution | +| design note, merged | **definition admission + invariants** | ratification admits terms and pins invariants — a normative spec, in force | +| owner's merge | **editorial acceptance** | accept, camera-ready, and publication of record in one act; the merge log is the record | +| PR review rounds | **shepherding — internal referee report** | revision-under-supervision until acceptable | +| amendment (A-series) | **erratum / addendum** | append-only, warranted, on the record; the original stands annotated | +| supersession ∧ erratum | **correction — retraction and replacement, reason stated** | the ratified correction composition (dn-erratum-relation) | +| build plan | **proof obligation** | §7's acceptance + falsifier pairs are statement + refutation condition | +| journal | **lab notebook** | contemporaneous working record — judgement, surprises, dead ends | +| issue `type:defect` | **counterexample** | a witness against a claimed property | +| issue `type:investigation` | **conjecture / hypothesis** | "establish or falsify" is the conjecture register | +| issue `type:ruling` | **axiom / postulate** | admitted by authority, not proven; filed closed because it IS the record | +| deskcheck | **artifact evaluation — Functional criteria** | "show it working, owner has final say", with the owner as evaluator | +| golden set | **benchmark, frozen** | fixed evaluation target, human-only changes | +| `CONSTITUTION.md` | **axioms / postulates** | the outermost admitted frame every agent inherits — never derived, never auto-modified | +| property test, green | **"tested — no counterexample found"** | a mechanized falsification attempt, survived | +| structure-instantiation | **model of a known structure** | proven theorems import under stated hypotheses — the honest "first principles" | +| fresh-agent test | **reproduction — in-house analog** | a party other than the authoring session re-derives from artifacts alone | +| one-way artifact chain | **preregistration-style trail (analog)** | capture is timestamped before design before build | +| parked + re-entry | **open problem, with reopening condition** | future work that names what would reopen it | + +**Where the mappings break — the fourth clause, previewed.** The glossary carries these +in full; recorded here so the map cannot be read stronger than it is: + +- *Capture → conjecture:* capsules also carry mood and direction, which are not claims. +- *Merged note → definition:* never a theorem — the worked entry below is the register's + cardinal lesson. +- *Merge → acceptance:* it is not refereeing; see the shepherding break. +- *Shepherding:* reviewers here share the author's incentives — say "internally + reviewed", never "peer-reviewed" (R2). +- *Amendment → erratum:* the house form is append-only and warranted; whether that is + stronger than venue practice is an unmeasured comparative, and stays unclaimed. +- *Correction:* the house term is deliberately the **composition** — plain + supersession-with-warrant is *replacement* (was once right; the everyday analogs are + arXiv v2 and RFC "obsoletes"), not retraction (was never right). Only + supersession ∧ erratum earns the retraction register (dn-erratum-relation, ratified + 2026-07-27: *a correction is a supersession composed with a warranted retraction*). + And community "retraction" additionally connotes fatal error or misconduct — routine + design evolution must not borrow that weight. +- *Build plan → proof obligation:* a category difference, named plainly — in + formal-methods practice an obligation is *discharged only by proof*; one not proven is + *open*. The house discharges by tests, so the honest status is "supported, obligation + open", never "discharged". The term teaches the shape (statement + what would refute + it), not the standard of discharge. +- *Journal → lab notebook:* regulated notebooks are tamper-evident and witnessed; a + journal is self-authored markdown, mutable until merged. +- *Defect → counterexample:* some defects refute nothing stated — they are just bugs. +- *Investigation → conjecture:* a settled investigation later work cites may earn + **lemma** — but that promotion is a **house rule stricter than the community's**: in + the literature "lemma" is an authorial label at write time (auxiliary intent), and + earned-by-citation naming is folklore about famous lemmas, not the label's meaning. + The glossary presents it as house-stricter-than-community, never as the community + meaning. +- *Ruling → axiom:* axioms are minimal by taste, criticized via independence and + consistency; rulings are operational by need, criticized by filing an issue. And the + register says **axioms**, not "axiom schema" — schema is a precise term of art (a + template with metavariables generating axiom instances: PA induction, ZF separation) + that nothing here instantiates. +- *Deskcheck → artifact evaluation:* the evaluator is not independent — criteria are + self-assessed; no badge is held or implied (§2.4.3). +- *Golden set → benchmark:* single-project; no community baselines attach. +- *Property test:* never shortens to "proven"; that word is reserved (§2.3.3). +- *Structure-instantiation:* transfer holds only while the stated hypotheses do. +- *Fresh-agent test:* ACM "Results Reproduced" requires another *team*; always say + "analog". +- *One-way chain → preregistration:* the fullest break in the register — the worked + entry below. +- *Parked → open problem:* open problems are announced to invite anyone's attack; + parked items address the house's own future selves. + +**Four worked entries, to fix the teaching shape** (the glossary carries all of them at +this depth): + +- *Theorem vs. ratified note.* A theorem is descriptive and proven: the world already + behaves this way, and here is the complete argument. A ratified design note is + prescriptive and admitted: the system *shall* behave this way, because the owner + merged it. Conflating them is the register's cardinal failure — a spec cannot be + true, only in force. +- *Deskcheck vs. artifact evaluation.* The ACM ladder (policy v1.1, five badges, three + families) puts "Evaluated–Functional" at: documented, consistent, complete, + exercisable, with evidence of verification. That is the deskcheck's exact question, + with the owner as the evaluation committee — a *criteria self-assessment*, since + badges are conferred by independent evaluation and nobody self-awards one. What the + house cannot claim: "Results Reproduced" (requires a party other than the authors — + the fresh-agent test is the honest *analog*) and "Results Replicated" (no in-house + analog exists; never claimed). +- *Ruling vs. axiom.* Both are admitted, not proven, and both are load-bearing + downstream. The difference is criticism: an axiom is challenged by independence and + consistency arguments; a ruling is challenged by filing an issue. The mapping holds + because deduction downstream treats both as given; it breaks because rulings are + revisable by their author and axioms, once a literature builds on them, effectively + are not. +- *Preregistration vs. the one-way chain.* Preregistration, as the community practices + it, means hypotheses **and an analysis plan** lodged with an **independent registrar** + (OSF, AsPredicted) *before* data collection. The chain has something real but + different: a timestamped design trail — capture before design before build, hardened + at each merge. The breaks: (a) the registrar is the author — the repo is + owner-controlled and branch history is mutable until merge, so the strongest + timestamp is the merge commit, not a third-party lodgment; (b) the registered object + is a design trail, not hypotheses plus an analysis plan, which is what anti-HARKing + protection is actually about; (c) no comparative to industrial practice is claimed — + that would be an unevidenced comparative of exactly the kind §2.3.3 prices. What + survives, stated precisely, is still worth having: **a preregistration-style trail, + in-house analog** — and nothing more (R8). + +### 2.3 The claim ladder — what each label costs + +**The principle.** A claim label encodes proof status and importance — never +enthusiasm. The ladder exists so that over-claiming becomes a *review-visible* defect: +after RR-2, a label is a checkable assertion about the evidence in the same +artifact, and review rejects mismatches the way it rejects failing tests. + +#### 2.3.1 The rungs + +| label | what earns it | agent-authorable? | +|---|---|---| +| **Definition** | introduces a term; no truth value; criticized as ill-formed or unmotivated, never false | yes | +| **Observation** | true by inspection or a raw measurement, pinned to a sha / run id | yes | +| **Remark** | commentary, explicitly non-load-bearing | yes | +| **Conjecture** | precise, falsifiable, believed, unproven — the falsifier named at birth | yes | +| **Hypothesis** | empirical register: a testable explanation; only ever *supported* or *falsified* | yes | +| **Claim** | an assertion the same artifact's evaluation section is contractually obliged to support | yes, with the evidence attached | +| **Proposition** | proven *relative to stated premises* — cited invariants, structure hypotheses, arithmetic domain; proof inline, checkable | yes — **the agent ceiling** | +| **Lemma** | proven auxiliary that earns the house name by later *use* (stricter than the community label — §2.2) | proof yes; the name, retrospectively | +| **Theorem** | proven, important, standalone — a complete written proof (machine-checked when Lean unparks) | effectively no; absence is honest | +| **Corollary** | immediate from a stated labeled result; proof short or omitted | yes, from a labeled result only | + +The ceiling rule, stated plainly: **agent-authored claims cap at Proposition-with- +checkable-inline-proof or Claim-with-named-falsifier.** This is not modesty theater — +it is the bar the book's preamble already sets (`Proposition` there is "a consequence +the manual DERIVES from a cited invariant — its proof is given inline and is checkable +by the reader; it asserts nothing the record does not", `preamble.tex:50-53`), promoted +from book convention to chain-wide policy. "Theorem" without a checked proof is the one +register error the research community treats as fraud-adjacent; the palace will simply +never make it, because the ladder gives every weaker-but-honest rung a name. + +Two guards on the rung agents will use most, because a plausible-but-wrong inline proof +— not Theorem abuse — is the realistic inflation channel: + +- **"Proven" in a Proposition always means relative to admitted premises.** The + premises are cited (invariants, structure hypotheses, arithmetic domain), and the + proposition asserts nothing the record does not. Un-anchored "proven" is the + theorem-conflation of the first worked entry, and review treats it as such. +- **Executable Propositions pair a property test with the prose proof.** Where the + labeled statement is checkable by machine, the falsifier is written and run — the + laws-ledger pattern (§2.3.2, item 3) generalized. A prose proof alone is the weakest + verification the house accepts anywhere; the pairing keeps the ladder on the same + mechanized-falsification footing as everything else. Falsifier F2 patrols both + guards. + +#### 2.3.2 Where labels attach + +1. **Design notes** — §2 decisions may carry labels. The native registers are + Definition and Invariant (admitted, in force); anything labeled Proposition carries + its proof inline. Wired as template teaching comments, not new frontmatter. +2. **The deskcheck paper** — its Definitions-and-claims section (§2.4.3) is written in + ladder labels; its Evaluation section discharges every Claim or says so honestly. +3. **The laws ledger** (sibling arc, when built) — each algebraic law lands as a + labeled claim (typically Claim, or Proposition with its paired falsifier) with one + falsifier per law; the label column is specified here so the sibling note consumes + it, never redefines it. +4. **The book** — the amsthm registry in `docs/book/preamble.tex:43-62` (principle, + invariant, proposition, devolution) extends with conjecture / definition / lemma / + theorem / corollary / remark environments and `\autoref` names, under a + scribe-contract plan. One taxonomy, one home — never a parallel set. Ordering note: + after RR-3 the claim environments live in the factored `docs/latex/palace-macros.tex` + (§2.4.5); whichever of the scribe sync and RR-3 lands second targets the file where + the environments then live, not a stale line pin. +5. **Issues** — no new labels. The lexicon's mapping (defect ≈ counterexample, + investigation ≈ conjecture, ruling ≈ axiom) is descriptive teaching, not taxonomy + change; the `type:`/`route:` grammar is frozen (§2.1). + +#### 2.3.3 Reserved words and the arithmetic-domain rule + +The words below are load-bearing in the research register; after RR-2 their use +costs what the community charges: + +| word | costs | +|---|---| +| **proven / proof** | a complete checkable argument exists in or is cited by the artifact; a green property test is "tested", "no counterexample found" | +| **significant** | a statistical test was run and is named | +| **optimal** | an optimality proof; otherwise "best measured" | +| **correct** | a stated spec and verification against it; otherwise "conforms to tests" | +| **novel / first** | a recorded literature search; the house default is the opposite claim — instantiation of a *known* structure, which is the credible direction | +| **complete** | an enumeration or exhaustiveness argument | + +And the domain rule, from the capsule's named foundational risk: **every algebraic or +equality claim states its arithmetic domain.** "Holds exactly over ℤ / exact +rationals; holds up to ε = over float64." Float addition is non-associative; +exact-equality claims over floats are precision theater, and the ladder forbids them. + +### 2.4 The deskcheck becomes a paper — same artifact, deeper genre + +#### 2.4.1 The genre decision + +A deskcheck is not a full research paper and pretending otherwise would be register +inflation (§2.5). The genre it already *is* — "show it working, or its honest current +state, with the evaluator holding final say" — has a name in the community: +**the artifact-evaluation report / artifact appendix**. Short (target 4–8 pages), +evidence-dense, self-assessing against the pinned ACM v1.1 criteria (no badge is held +or implied — §2.4.3). That is the format adopted. + +#### 2.4.2 Carrier, lifecycle, and the form choice — the compatibility spine + +**Nothing about the `dc-` lifecycle changes.** Verified at HEAD: `scripts/board.py` +globs `docs/deskchecks/*.md`, requires `type: deskcheck`, and reads exactly +`{id, track, verdict}`; closure is computed, never flipped; the queue derives from +manifests. So: + +- **The carrier stays `docs/deskchecks/dc-NNN.md`** with the front-matter schema + byte-compatible (`type, id, track, date, items, audit_refs, verdict, send_back, + links`) and the four house sections retained — What was built · How · Surprises · + What is NOT done. Three of them may shrink to short paragraphs pointing into the + paper; **How keeps the runnable demo commands in full** (or points at a plain sibling + script, `docs/deskchecks/dc-NNN/demo.sh`). The carrier alone must pass the + fresh-agent test with no LaTeX toolchain installed: the tree stays self-sufficient; + the paper deepens — recorded outputs, tolerances, figures — it never gatekeeps. +- **The form is chosen when the track is picked, before a word is authored.** Every + deskcheck is track-closing (closure is computed from the approved dc, so a + "track-closing deskchecks only" qualifier would be vacuous) — which makes the choice + point the whole game. The owner names paper or short form when he picks the track off + the queue; absent an owner pick, the agent proposes the form in the dc PR *before* + writing the paper, never after the cost is sunk. **For the five currently-owed tracks + the default is the short form** — draining real debt without waiting on RR-3, and + minting the closure baseline F6's supplementary clause needs. The paper becomes the + default *proposal* only after the owed queue drains; the short form remains legal + forever. The four-question core is the invariant; the paper is the deepening, priced + in §3 (falsifier F6 patrols the boundary). +- **The paper source lives at `docs/deskchecks/dc-NNN/main.tex`** (one directory per + deskcheck, TikZ/pgfplots figures as sibling `.tex` files per book convention). +- **PDFs are never committed.** `docs/deskchecks/.gitignore` replicates the book's + source-only precedent (`*.pdf`, `*.aux`, latexmk residue). Delivery rides the + existing exhaust lane: the compiled `main.pdf` is copied to + `~/.mind-palace/exhaust/reports/dc-NNN.pdf` (Syncthing → phone) — the lane the phone + build report already uses. No new channel; at deskcheck time the PDF *absorbs* the + phone report's role for that track (full retirement of the HTML report is parked). +- **`board.py` changes by zero lines.** A compatibility test (RR-3) asserts a + paper-era dc closes its track and renders in the queue; `tests/unit/test_board.py` + and the dormant-gate integration suite stay green unmodified. + +#### 2.4.3 The section spine — the four questions, grown up + +Adapted from empirical-CS practice and the artifact-appendix shape, with the house's +four headings surviving as the spine's load-bearing members: + +| paper section | carries | house ancestor | +|---|---|---| +| Abstract | track, claims evaluated, verdict-relevant headline, criteria self-assessment | — | +| 1 Motivation | why the track exists — the manifest's warrant and dod, cited | track manifest | +| 2 Definitions & claims | ladder-labeled claims this artifact supports; scope of claims stated | — | +| 3 What was built | design → implementation, every assertion `\artifact`/`\coderef`-pinned | **What was built** | +| 4 Evaluation | the demonstration record: observed outputs **with tolerances**, per-dod-criterion results | **How** | +| 5 Surprises & discussion | what building revealed; negative results in full | **Surprises** | +| 6 Threats to validity | what is NOT done; construct/internal/external threats; the float-ε caveat where it applies | **What is NOT done** | +| 7 Availability & provenance | repo refs, the paper's edition sha, how to re-run; who drafted, who evaluated, how it landed | — | +| References | verified-only; DOIs recorded in-repo, never [FROM MEMORY] | external-grounding gate | + +The Evaluation section records what the carrier's demo script produced — the runnable +commands live in the carrier (§2.4.2), the paper carries the observed outputs with +tolerances, so the waived short form and the fresh-agent test stay coherent. + +**The provenance statement is required, not decorative.** These papers are +agent-drafted, and research-community norms now expect generative-AI involvement +disclosed in manuscripts [FROM MEMORY — stable practice since 2023]. The house already +treats agent-vs-owner authorship as a first-class coordinate +(`docs/design-notes/authorship-distance-axis.md` — dn-authorship-distance-axis, the +authorship-distance design, *draft* at HEAD, leaned on as an idea, not cited as +ratified). The honest statement is a strength, not a confession, and the template +hard-codes its shape: *drafted by under supervision; evaluated by the +owner against the live demo; landed by the owner's merge.* + +**The criteria self-assessment, phrased so it cannot inflate.** The template pins the +ACM v1.1 definitions — five badges, three families — and the paper states which +*criteria were met and by whose evaluation*, never that a badge or rung was "achieved" +(badges are conferred by independent committees; nobody self-awards one). The in-house +maximum reads: "meets the 'Artifacts Evaluated – Functional' criteria; evaluator: the +owner — a self-assessment against the pinned definitions; no ACM badge is held or +implied", plus the fresh-agent reproduction *analog* when a fresh session re-ran the +demo from merged artifacts alone. "Replicated" is never claimable and the template says +so. The pinned definition text carries its verification source and date, re-verified +against the fullest available primary quotation at RR-3 build time — this note's +verification ran through SIG mirrors because acm.org refuses automated fetches, which +is good enough for a design note and not for a standing pin (R6; filed as an issue). + +Rules carried over from the book: assert nothing uncited (`\artifact{}` for design +claims, `\coderef{}{}` for implementation); one edition marker per paper (the `\gitref` +pattern, pinned at the demo sha); notation extends `docs/book/notation.tex`, never +forks it; figures are TikZ/pgfplots, text-only, no binary assets. + +#### 2.4.4 The evidence and the verdict — the tension, resolved explicitly + +The paper **carries** the evidence; it does not **replace** the owner's live approval. +The carrier's How is the demo *script*; the paper's §4 is the demo *record* — the owner +runs the script at the keyboard, per the deskcheck discipline; the paper is what makes +his evaluation repeatable and reviewable away from the keyboard (the exhaust-lane PDF), +not what substitutes for it. + +How a verdict lands post-regime — the gap, stated exactly: the store's own README +(`docs/deskchecks/README.md`) specifies only the *pre-regime* mechanics — gate-guard +denial, the lazygit blessing ceremony, "the third owner-only gate" beside two retired +flips — and no artifact at HEAD writes the post-regime translation. Closed here: +**a dc lands by PR like everything else.** The agent authors the whole bundle (carrier ++ paper) with `verdict: pending` — the only agent-legal value, unchanged. At the +deskcheck session the owner runs the demo, sets `approved` or `needs-work` (+ +`send_back`) **by his own hand in that PR**, and merges; the merge carries the verdict, +and `board.py` computes closure from the merged field exactly as today. The verdict +field survives as the one hand-set value because closure is *computed from it* and +because a pure merge-equals-approval reading would lose `needs-work`/`send_back` +expressiveness and force a board change for nothing. Agents still never touch it. +[INFERENCE — this regime translation is this note's proposal; nothing at HEAD +specifies it, and the owner confirms or corrects it at ratification. The ruling ask is +filed as a `route:owner` issue alongside this PR so the decision is citable either way; +meanwhile the owner's merge of this note adopts the recorded default. The +deskcheck-verdict *signing* question stays parked exactly where +dn-typed-workflow-registry (ratified 2026-07-27 — the sign-based-security design) left +it.] + +#### 2.4.5 Toolchain and the DRY factoring + +Toolchain: **the book's, unchanged** — `latexmk -pdf` (pdflatex; MacTeX at +`/Library/TeX/texbin`; tectonic is not installed and is not introduced). Compile: +`cd docs/deskchecks/dc-NNN && latexmk -pdf main.tex`. + +The shared layer: the citation macros, claim environments, and house colors currently +live in `docs/book/preamble.tex` and are needed by an `article`-class paper. RR-3 +factors them into **`docs/latex/palace-macros.tex`**, `\input` by both the book's +preamble and the paper template's — one definition, two consumers. **The factoring has +design content, and the plan says so plainly, twice over:** (a) the theorem +environments are `[chapter]`-numbered (`preamble.tex:46,55,57`) and `article` has no +chapter counter — they cannot lift verbatim; the macros file takes its numbering parent +as a parameter, or the environment definitions stay per-consumer and only the +counterless layer (citation macros, colors, `\fwdthesis`) is shared — RR-3's builder +decides which, as design scope, not as a surprise. (b) `\gitref` is the book's edition +marker and stays per-document — the book pins its edition, each paper pins its demo +sha. The move carries a two-sided compile obligation: the book builds cleanly and +renders page-identically after it, **and** the paper template compiles from the +skeleton (falsifier F4, both clauses). The include mechanism (relative `\input` vs +`TEXINPUTS`) and latexmkrc niceties remain build decisions. The notation registry +stays where it is — `docs/book/notation.tex`, single, extended never forked — and +papers `\input` it directly. + +### 2.5 The honesty denylist — over-claiming as a review-visible defect + +The register's credibility failure mode is decoration: research words doing prestige +work their evidence has not paid for. The rules below bind all register-bearing +artifacts and land in the glossary's front section; PR review enforces them the way it +enforces scope: + +1. **R1** — "Theorem"/"proven" only per the ladder (§2.3.1, §2.3.3). The cardinal rule. +2. **R2** — "internally reviewed" / "audited", never "peer-reviewed". The merge is an + editorial accept, not refereeing. +3. **R3** — criteria claims only per the pinned v1.1 definitions, phrased as *criteria + met + evaluator*, never as a badge or rung "achieved" — no ACM badge is ever held or + implied; "Replicated" never. +4. **R4** — no "novel"/"first" without a recorded search; the house's default posture + is structure-instantiation, which is anti-novelty and credible. +5. **R5** — standard names for known objects (Ollivier-Ricci curvature, W₁/Wasserstein + LP, finite Boolean algebra) — never house rebrands. Internal metaphors stay + internal: "our mini Langlands" never appears in a paper. +6. **R6** — citations verified-only (the external-grounding gate); no decorative or + from-memory references, in the deskcheck template as a hard rule. +7. **R7** — numbers carry tolerances; equality claims carry their arithmetic domain + (§2.3.3). +8. **R8** — the chain claim is "a preregistration-style trail (in-house analog)", with + the registrar-is-the-author break stated (§2.2's worked entry) — and nothing more. +9. **R9** — externally, the project is what it is: a single-investigator study whose + artifacts are agent-drafted and owner-reviewed, publishing internally reviewed + technical reports. That framing is credible and even distinctive; + "journal/lab/research program" cosplay is what actual researchers smell instantly. + +**Enforcement, priced honestly.** Under the merge gate the merging reviewer is the +owner, so R1–R9 are review load and this note does not pretend otherwise. Three +mitigations, none free but none ceremonial: the reserved-words table is grep-able and +agent pre-merge audits grep it; the paper template hard-codes the phrasings that +inflate most (the provenance block, the criteria wording); and the ladder makes the +honest label the path of least resistance. The owner's read is the last wall, not the +only one. + +### 2.6 The empty slot — the research Question + +A paper opens with a question. The palace, at HEAD, has none stated — the study has no +owner-authored research Question, and authoring one is owner-only by standing rule. +The register makes this absence *visible* rather than filling it: the glossary's front +matter carries the slot explicitly ("Research Question: unwritten — owner-only"), and +the deskcheck paper's Motivation section cites the track's warrant and dod, never a +global Question, until one exists. No mechanism nags; surfacing is the design's whole +obligation here. When the owner writes the Question, it becomes the anchor every +paper's Motivation may cite — and the strongest single credibility move available to +the project, because a stated question converts a collection of artifacts into a study. + +## 3. Consequences + +**On the owner's merge of this note, and not before** — three graduation licenses, +session-sized, dependency-ordered, split at graduation. They are named **RR-1/RR-2/ +RR-3** (research register), following the parent note's WF-N unit-naming precedent — +"track" stays reserved for the board's own coordinate, per §2.1's invariant applied to +this note itself: + +- **RR-1 — the lexicon.** Deliverable: `docs/lexicon.md` with every §2.2 map row as a + complete entry per the contract (four clauses + verification status), the honesty + denylist (§2.5), the Question slot (§2.6), and one-line register pointers in the + templates and skills that traffic in mapped terms. The workflow manifest gains its + working-material rows in the same diff — three DoD lines (RR-1/2/3) and a one-clause + scope extension — a D1-licensed edit ("owner or orchestrator may add; only a + deskcheck closes"), so the lane's own deskcheck can see this work. De-staling rides + along: any template/skill line this unit touches that still carries retired mechanics + (gate-guard, hand-flips, `/graduate refuses`) is rewritten to merge-gated language + *in the same diff* — touched files never re-propagate dead regime. Falsifier: any + entry missing its where-it-breaks clause or its verification status; or the owner's + cold-read spot-check (F5) fails. +- **RR-2 — the claim ladder wired.** Gated on RR-1 (labels are lexicon entries). + Deliverable: ladder + reserved-words + domain-rule conventions into + `docs/templates/design-note.md` and `docs/templates/build-plan.md` as teaching + comments; the issue skill's descriptive mapping paragraph; a minted scribe-contract + item extending the book's amsthm registry (`preamble.tex:43-62` pattern, `\autoref` + names, notation untouched; post-RR-3 home is `palace-macros.tex` — §2.3.2's ordering + note). Falsifier: F2 — a post-RR-2 merged artifact labels property-test evidence + "proven", or a Proposition lands past its guards, and review passes it. +- **RR-3 — the deskcheck paper.** Gated on RR-2 (the paper writes in ladder labels). + Deliverable: the evolved `docs/templates/deskcheck.md` (carrier, schema + byte-compatible), the `docs/templates/deskcheck-paper/` LaTeX skeleton (spine of + §2.4.3, provenance block, criteria definitions pinned with recorded verification + source per R6), `docs/latex/palace-macros.tex` factored with the two-sided compile + obligation (§2.4.5), `docs/deskchecks/.gitignore`, **`docs/deskchecks/README.md` + rewritten to the §2.4.4 mechanics** (it still teaches the retired lazygit/gate-guard + ceremony — filed as a defect issue with this PR), the exhaust-lane delivery step, and + the board compatibility test. Falsifiers: F3 (board), F4 (compile, both sides). + +**Priced, so the owner ratifies with the bill visible.** The short-form carrier is +minutes of agent work and a 1–2 page read. A paper is a dedicated authoring session per +deskcheck — order 5–10× the carrier — plus the owner's review of a 4–8 page PDF and its +`.tex` diff on top of the same live demo. The exhaust-lane PDF moves that review +off-keyboard; it does not shrink it. The five currently-owed tracks default to the +short form (§2.4.2), so the owed queue costs nothing new; the paper's bill starts only +where the owner picks it, and F6 fires if a bundle ever exceeds one authoring session. + +**Independence declared, so nobody serializes what need not wait:** the five +currently-owed deskchecks (agentic-loop, fiber-geometry, inner-outer-core, ops, +sync-diac-dreamers) do **not** wait on any of this — they default to the 17-line short +form, and the queue never blocks on a design note. The sibling foundations note (§1.3) +proceeds independently; only the label definitions are shared, and they are frozen +here. + +**First real exercise — two artifacts, not one.** The first paper-format deskcheck is +an owner session off the existing queue — his pick of track — producing that track's +`dc-NNN` as the first paper. That *exercises* the RR-3 pipeline; it does not close this +note's own lane. Closing the workflow lane still requires an approved dc naming +`track: workflow` (computed closure, `board.py:309-327`), evaluated against the +manifest's RR rows — the board's phase function does not care which pipeline the dc was +typed in. + +**Explicitly NOT licensed:** the laws-ledger sweep (sibling arc); Lean; authoring the +Question; retiring the HTML phone report; disposing of the dormant gate machinery; +book chapter content beyond the registry extension; any parser change. + +## 4. Wiring & enablement + +**How it wires:** `docs/lexicon.md` (new, authored); one-line register pointers in +`docs/templates/{design-note,build-plan,deskcheck,capsule}.md` and the issue/pr/ +checkpoint skills; ladder teaching comments in the design-note and build-plan +templates; the workflow manifest's DoD rows (D1-licensed working material); +`docs/templates/deskcheck.md` evolved in place (carrier schema byte-compatible) plus +`docs/templates/deskcheck-paper/main.tex` (spine, provenance block, pinned criteria +with verification source, `\input` of `docs/latex/palace-macros.tex` and +`docs/book/notation.tex`); `docs/latex/palace-macros.tex` factored from +`docs/book/preamble.tex` with the counter-parent question resolved as RR-3 design +scope and the book re-pointed at it; `docs/deskchecks/.gitignore` (book precedent); +`docs/deskchecks/README.md` rewritten to the post-regime verdict mechanics; the +compile target documented in the template (`cd docs/deskchecks/dc-NNN && latexmk -pdf +main.tex`); the delivery step copying `main.pdf` → +`~/.mind-palace/exhaust/reports/dc-NNN.pdf` (existing Syncthing lane; whether as a +documented command or a small extension of `scripts/exhaust_report.py` is a build +decision); a board-compatibility test asserting a paper-era dc closes its track. +`scripts/board.py`: zero lines. `CLAUDE.md`: zero lines. + +**What it takes to flip it on:** (a) RR-1 merges → the glossary is live on read; +(b) RR-2 merges → the next authored note/plan carries the ladder, live on first +use; the registry extension lands at the next scribe sync; (c) RR-3 merges → the +pipeline is runnable end-to-end: template → `latexmk` → PDF → exhaust lane. The +owner's only hand-acts: pick a track off the deskcheck queue *and name the form*, sit +the deskcheck session, run the carrier's demo script, set the verdict by hand, merge +the dc PR — the same acts the deskcheck discipline always required, now optionally +producing a paper. No daemon flag; this is workflow tooling — `mind-palace deploy` is +not involved. + +## Parked decisions + +| decision | default recorded | re-entry condition | +|---|---|---| +| Lean / proof-assistant adoption | not adopted; "Theorem" stays effectively unreachable | a claim a property test cannot falsify (capsule park, unchanged) | +| external venue / arXiv / DOI | none — internally reviewed technical reports only | the owner authors the Question and wants external referees | +| brainstorm capsules adopting the register | chat stays vernacular; capture template gains only the Conjecture gloss (RR-1) | owner asks, after living with RR-1 | +| HTML phone build report | kept for mid-track build waves; the dc PDF absorbs the track-closure role | two paper deskchecks delivered → owner reviews the overlap | +| dc verdict mechanics (§2.4.4) | owner-hand field, landed by his merge; agents write only `pending` | the `route:owner` issue filed with this PR — merging this note adopts the default | +| dormant deskcheck-gate machinery | untouched — carrier stays shape-compatible, tests stay green | a hooks-disposition sweep opens, or the tests redden (the `parked` issue with this PR) | +| lexicon drift maintenance | no standing sweep minted; entries carry verification status | an entry teaching a retired mechanic or stale term — a `type:defect` reopens RR-1 for it | +| bibliography tooling | manual `thebibliography`, DOI-verified entries (the SYNC.md pattern) | a single paper exceeds ~10 external references | +| the research Question | slot exists, empty, labeled empty | owner-only authorship, any time — not a condition of anything here | + +The dormant-machinery row's members, named (this half is prose, not a cell): +`.claude/hooks/gate-guard.sh`, `_lib.py`'s verdict clauses, and the 346-line +`tests/integration/test_deskcheck_gate.py` — all green-but-dormant at HEAD. + +## Falsifiers — what would prove this design wrong + +The owner ratifies falsifiers, not proofs. + +- **F1 (alias invariant):** any RR-1..3 merge renames a machine-parsed string + (§2.1's enumerated list) without its parser in the same diff, or breaks an existing + id or command. Grep-checkable at review; one occurrence voids §2.1. +- **F2 (bar raised, not decorated):** a post-RR-2 merged artifact carries + "Theorem"/"proven" over property-test-only evidence; **or** a merged Proposition's + inline proof fails a cold-check; **or** an executable Proposition lands without its + paired falsifier — and review passes it. The ladder then decorates instead of + binding, and §2.3 has failed as policy. +- **F3 (board compatibility):** a paper-era dc fails to move its track to CLOSED, or + the queue misrenders it, or `test_board.py`/`test_deskcheck_gate.py` redden without + intentional cause. The carrier contract (§2.4.2) is then broken. +- **F4 (DRY compile parity, both sides):** after the `palace-macros.tex` factoring the + book fails `latexmk` or renders divergent pages, **or** the paper template fails to + compile from the skeleton. The shared layer then forked instead of factored, and + §2.4.5 must be redone. +- **F5 (the glossary teaches):** the owner cold-reads three glossary entries and cannot + recover house meaning, research meaning, and the breaking point. The lexicon then + renames instead of teaching, and RR-1's deliverable is not done. +- **F6 (evolution, not ritual):** a dc bundle (carrier + paper) exceeds one authoring + session; or the owner declares at a verdict session that the paper delayed his + verdict; or a track is waived to the short form because the paper felt too heavy. + Any one firing shrinks the default to carrier-only and the paper becomes opt-in. + (A relative clause — median time-to-closure versus the short-form baseline — only + becomes measurable once short-form closures exist; the five owed tracks defaulting + short-form mints that baseline, and the clause then activates as a supplement, never + as the operative test. At HEAD zero deskchecks have ever been recorded, so no + baseline exists yet and this note does not pretend one does.) +- **F7 (register inflation):** any merged artifact says "peer-reviewed", claims a + badge or an unmet criterion, or carries an internal metaphor in external register. + The §2.5 denylist then failed at review, and its rules move from glossary prose into + the pr skill's audit guidance as a grep-able list — not a new ceremony, a sharper + grep. + +## Cross-references + +Code and templates (all at `68d8d39`): `scripts/board.py:283-294` (dc scan — the +front-matter contract §2.4.2 preserves), `:309-327` (computed closure), `:445-494` +(queue rendering); `docs/templates/deskcheck.md:1-17` (the carrier, evolved in place); +`docs/deskchecks/README.md` (pre-regime verdict mechanics — rewritten in RR-3, never +propagated); `docs/book/preamble.tex:28` (`\gitref` edition marker), `:30-35` +(`\artifact`/`\coderef`), `:43-62` (the amsthm registry §2.3.2 extends), `:46,55,57` +(the `[chapter]`-numbered environments behind §2.4.5's counter-parent scope); +`docs/book/notation.tex:1-4` (the single symbol registry); `docs/book/.gitignore` (the +source-only precedent); `scripts/readmap.py:27`, `scripts/capsule.py:41,62` (frozen +parse points, §2.1); `.claude/skills/issue/SKILL.md:24-38` (the label taxonomy the +lexicon maps); `.claude/skills/book/SKILL.md` (LaTeX conventions authority); +`.claude/skills/checkpoint/SKILL.md` (the fresh-agent test — the reproduction analog). + +Artifacts, glossed: `docs/brainstorms/mathematical-foundations.md` (the warrant capsule, +PR #42, sequenced first — owner seeds 1–2, the terminology seeds, +structure-instantiation, the falsifiers-before-proofs epistemology, the float-ε risk); +`docs/design-notes/track-board-and-deskcheck-gate.md` (dn-track-board-and-deskcheck-gate, +ratified 2026-07-21 — D2's derived board untouched; D3 minted the deskcheck artifact +this note evolves, and D3's verdict-hook mechanics predate the merge-gated regime and +are not propagated; D1 licenses the manifest DoD edit); +`docs/design-notes/erratum-relation.md` (dn-erratum-relation, ratified 2026-07-27 — the +correction composition the lexicon's retraction row maps); +`docs/design-notes/external-grounding.md` (dn-external-grounding, ratified — the +verified-citation gate, R6); `docs/design-notes/dn-typed-workflow-registry.md` +(dn-typed-workflow-registry, ratified 2026-07-27, pre-regime — parks deskcheck-verdict +signing; park preserved §2.4.4); `docs/design-notes/authorship-distance-axis.md` +(dn-authorship-distance-axis, *draft* at HEAD — authorship distance as a first-class +coordinate; the provenance block's conceptual ancestor, not a ratified citation); +`docs/DESKCHECK-QUEUE.md` (derived — the five owed tracks, never hand-edited); +`docs/tracks/workflow.md` (this note's track manifest, pre-existing; gains RR DoD rows +in RR-1). + +External (per the external-grounding gate): ACM Artifact Review and Badging v1.1 badge +definitions — VERIFIED 2026-08-09 via sigir.org and sigsim.acm.org quoting the policy +(acm.org itself refused the fetch; re-verification against the fullest primary source +is an RR-3 obligation, filed as an issue); AE practice at SOSP/OSDI/EuroSys/ATC/FAST — +VERIFIED via sysartifacts.github.io. Claim-ladder community norms, the empirical-paper +spine, the threats-to-validity taxonomy, the AI-disclosure norm, **and the +research-meaning glosses of the §2.2 map wholesale** (preregistration practice, +shepherding, the retraction genre, axiom-criticism norms, the artifact-appendix shape) +are stable community practice carried here as [FROM MEMORY] — admissible in a design +note, barred from any paper bibliography until verified per R6; RR-1's glossary +records per-entry verification status so the distinction survives into the artifact +that teaches it. \ No newline at end of file From f9070365859969280de83fbf3c6e9cb6391d414b Mon Sep 17 00:00:00 2001 From: Alberto Serrano-Calva Date: Mon, 10 Aug 2026 15:17:19 -0400 Subject: [PATCH 2/2] =?UTF-8?q?design(mathematical-foundations):=20the=20f?= =?UTF-8?q?rame,=20the=20laws=20ledger,=20and=20the=20Lean=20ladder=20?= =?UTF-8?q?=E2=80=94=20the=20overhaul's=20second=20note?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Structure-instantiation as the foundation (each component names the structure it models, states its hypotheses, imports theorems only under them; the implemented correspondences tabled as the working bridges). The laws ledger: docs/LAWS.md, seven mandatory columns, ~30 seed rows extracted from the real code (memberships first — resolved as coordinate-keyed relation with multiset projection, NOT the capsule's Boolean algebra; Boolean structure survives only in the support image, stronger readings demoted to Conjecture with a named falsifier). The Lean ladder L0-L4 adopted from issue #48: formal/ as a zero-coupling sibling, L1 statements with Plausible attacks and a sorry ratchet guarded against the axiom escape, L2 entry-gated discharge, L3/L4 parked. Float-epsilon as substance: three arithmetic tiers named and bound. Adversarially audited: 5 lenses (house rules, math-correctness vs code, regime/consumed-interfaces, feasibility x2), 6 must-fixes + ~25 should-fixes applied in revision — among them a fabricated code quotation replaced with the real text, the chi_s windowed-call counterexample recorded as a stated hypothesis, GAP-capped labels brought under the register's ceiling, anchor semantics fixed to symbol-at-HEAD with the repair model stated, and the SimpleGraph-vs-weighted Mathlib transfer priced honestly. Rides with: eight surgical edits to dn-research-register (its parked Lean row now points at the ladder; sect 1.3 names the real file) and the new track manifest docs/tracks/mathematical-foundations.md (owner adjudicates the coordinate at the merge). Warrant: owner seeds 1+3 (docs/brainstorms/mathematical-foundations.md, PR #42 + this session's directive); the Lean investigation is issue #48. --- .../dn-mathematical-foundations.md | 734 ++++++++++++++++++ docs/design-notes/dn-research-register.md | 33 +- docs/tracks/mathematical-foundations.md | 52 ++ 3 files changed, 806 insertions(+), 13 deletions(-) create mode 100644 docs/design-notes/dn-mathematical-foundations.md create mode 100644 docs/tracks/mathematical-foundations.md diff --git a/docs/design-notes/dn-mathematical-foundations.md b/docs/design-notes/dn-mathematical-foundations.md new file mode 100644 index 0000000..dade0d5 --- /dev/null +++ b/docs/design-notes/dn-mathematical-foundations.md @@ -0,0 +1,734 @@ +--- +type: design-note +id: dn-mathematical-foundations +track: mathematical-foundations # NEW manifest, minted in this PR (docs/tracks/mathematical-foundations.md) — ⚑ the owner renames or rejects the coordinate at the merge +status: draft # provenance description, never a gate (merge-gated regime, 2026-07-28) +created: 2026-08-09 +updated: 2026-08-09 +links: + - docs/brainstorms/mathematical-foundations.md # THE WARRANT (PR #42, capture branch — lands first; see Sequencing) — owner seed 1 + the structure-instantiation bridge + - docs/design-notes/dn-research-register.md # THE SIBLING (§1.3) — same PR #47; the §2.3 claim ladder consumed here; its parked Lean row now points at §2.4 below + - https://github.com/ascalva/mind-palace/issues/48 # the Lean investigation record — load-bearing external claims VERIFIED 2026-08-09 (its one [FROM MEMORY] row unleaned-on) + - docs/design-notes/connectivity-instruments.md # RATIFIED — CN-1..CN-7: σ*, the (σ,t) conductance profile, sign law, χ_s, forced helix + - docs/design-notes/core-graph-instruments.md # RATIFIED — P1 core self-containment, P3 one Laplacian, P4 no silent metric change + - docs/design-notes/magnetic-laplacian.md # RATIFIED (design-only) — the L^{(q)} fiber family; flux = abelianized holonomy + - docs/design-notes/temporal-retrieval-algebra.md # RATIFIED — A1–A8; π_active/σ_*, 𝔸 = d + τ, K(β), β* + - docs/design-notes/core-query-protocol.md # RATIFIED — §2.2 the query-mode algebra (tropical ↔ heat-kernel ↔ Gram via K(β)) + - docs/design-notes/vector-membership-store.md # IN FORCE by owner merges (150a190…c62ea7c lineage; status field is provenance) — the §4 membership math + - docs/design-notes/fiber-geometry.md # RATIFIED — FG-0 alphabet, FG-5 block-diagonal sheaf Laplacian + - docs/NOTATION.md # the symbol authority — staleness flagged in Cross-references, not fixed here + - docs/WHITEPAPER-FORMAL-PROPERTIES.md # the existing invariant tiering + property-test discharge scheme this note EXTENDS +supersedes: null +superseded_by: null +warrant: docs/brainstorms/mathematical-foundations.md # owner seed 1, 2026-08-09 — quoted in the opening blockquote; reaches main via PR #42, sequenced first +--- + +# Mathematical foundations — structure-instantiation, the laws ledger, and the Lean ladder + +> Composed at **fable** (`claude-fable-5`, xhigh, 2026-08-09). Per the +> banner-unreliability lesson (finding-0147, frozen history: a composed-at banner is a +> claim, not a proof), the owner cross-checks usage at review. Agent-drafted, filed as +> `draft` on a branch. Under the merge-gated regime (owner ruling 2026-07-28) nobody +> flips a status — **the owner's merge of this PR is ratification**, and the `status:` +> line above is provenance description, never a gate. If this text is on `main`, the +> owner put it there. +> +> **Sequencing:** this note rides **PR #47 beside its sibling, +> dn-research-register** (the research-register design — the claim ladder this note +> consumes), per owner seed 3 (2026-08-09: *"draft the foundations note, the laws +> ledger AND the Lean ladder, the full treatment … PR #47 can contain all the design +> notes, it's an overhaul"*). The warrant capsule lives only on the capture branch of +> PR #42 and is not at HEAD (`68d8d39`); that PR lands first — or this branch stacks +> on it — so both notes' warrant paths resolve in the tree the reviewer reads. **A +> third dependency:** the memberships store (the bp-152 lineage — the +> vector-membership-store build) is *staged in the owner's checkout, on no branch*; +> the MEM family reads it, so MF-1 is entry-gated on that store landing by its own +> PR. + +> *"the project's math is extensive — query algebras, Laplacians, curvature, sets and +> memberships, type correctness. What axioms do they rely on; can we derive from first +> principles; would that empower us; what stable foundation proves correctness? A +> captured idea is like a theorem/proposed definition — how far does the rabbit hole of +> implications propagate? Is foundational math the bridge to other branches — 'our mini +> Langlands'? Is this where a proof-based language comes in?"* — owner, 2026-08-09 +> (seed 1). +> +> The answer, in one sentence: **the palace's correctness does not rest on axiomatic +> descent — it rests on structure-instantiation: every component names the known +> structure it is a model of and imports that structure's theorems under stated +> hypotheses; the laws ledger makes those namings auditable law by law, and the Lean +> ladder makes the finite algebraic core machine-checkable, one priced rung at a +> time.** + +## 1. Purpose and scope + +### 1.1 What this note decides + +Five decisions, presented as one note because they are one move — the palace saying +exactly what mathematics it stands on, and building the two artifacts that keep the +saying honest: + +1. **The frame** (§2.1) — correctness by structure-instantiation, not first-principles + derivation. The palace's mathematics is finite in substance; "what axioms do we + rely on" resolves into "which structure is each component a model of, under which + hypotheses" — and the implemented correspondences between structures are tabled as + the working bridges. +2. **The laws ledger** (§2.2) — a single authored index, `docs/LAWS.md`, one row per + law: statement with arithmetic domain, claimed structure, code anchor, ladder + label, named falsifier test, formal status. The ledger *indexes* — it restates no + proof, no test, no Lean statement. A law without its falsifier test is at most + Conjecture, and the ledger makes that visible. That visibility is the point. +3. **Structure honesty** (§2.3) — the true structure of each component, named as + implemented; the known Boolean-algebra tension over memberships resolved on the + record's side; the temporal/query algebra's pinned-vs-conjectural line reported. +4. **The Lean ladder** (§2.4) — the L0–L4 adoption ladder from the Lean investigation + (issue #48, the Lean-adoption investigation; load-bearing external claims verified 2026-08-09) + adopted as design: `formal/` as a zero-coupling sibling package, L1 + statements-as-specs with a sorry-count ratchet, L2 agent-proved discharge, L3/L4 + parked with re-entry. +5. **Float-epsilon as substance** (§2.5) — the arithmetic-domain column is mandatory + ledger schema; the three arithmetic tiers the codebase already practices are named + and bound. This consumes the register's rule R7 and §2.3.3 (dn-research-register — + the sibling); the rule lives there, the substance lives here. + +How far the rabbit hole of implications propagates — capture-as-conjecture, deductive +closure through labeled steps — is the sibling's territory: a captured idea enters as +**Conjecture** and its implications propagate only through falsifier-carrying labeled +claims (dn-research-register §2.2, the capture → conjecture mapping; §2.3, the +ladder). Cited here, never repeated. + +The track is `mathematical-foundations` — a new lane, minted with this note (manifest +in this PR; the scored-beliefs/erratum-relation precedent: an agent mints the +coordinate alongside its founding note and the owner adjudicates it at the merge). No +existing lane honestly fits: `workflow` owns how work is framed and recorded — exactly +why the sibling lives there, and why its §1.3 carves this arc *out*; the foundations +substance (Laplacians, curvature, memberships, query algebras, the formal layer) +spans core-wide mathematics no manifest owns. + +### 1.2 Non-goals (load-bearing — read at ratification) + +1. **No Lean in `core/` — ever, in either direction.** `formal/` is a sibling package + like `eval/`: never imported by `core/`, importing nothing from it. The spec layer + is documentation-with-a-kernel-check, zero runtime coupling. [ESTABLISHED — core + self-containment (dn-core-graph-instruments P1) + issue #48 Axis D.] +2. **L3 and L4 are not licensed.** Float-ε formal bridges (FloatSpec-style) enter + per-claim only, and verified kernels stay parked; both carry recorded re-entry + conditions (Parked decisions). [ESTABLISHED — the ladder's own pricing, issue #48.] +3. **Ollivier–Ricci and Cheeger formalization are not licensed.** Both are absent from + Mathlib (issue #48, verified 2026-08-09; the W₁/KR layer of arXiv:2607.08986 is + the recorded on-ramp for the *Ollivier* side specifically); the house curvature + floor is Forman (§2.3.3), and L1 + formalizes definitions and stated laws only. [ESTABLISHED.] +4. **No golden-set or eval-fixed-point touch.** `CONSTITUTION.md`, `eval/golden/**`, + `eval/golden.py` are denylist surfaces; nothing here proposes them. + [ESTABLISHED — the fixed points.] +5. **The ladder labels are consumed, never redefined.** The rungs, the agent ceiling + (Proposition-with-checkable-inline-proof / Claim-with-named-falsifier), the two + Proposition guards, the reserved words, and the arithmetic-domain rule are the + sibling's (dn-research-register §2.3, frozen there); this note and the ledger use + them as given. [ESTABLISHED — the §1.3 boundary, both notes.] +6. **`docs/NOTATION.md` stays the symbol authority.** Its Family-5 staleness (it still + says `core/complex/` "does not exist yet") is flagged in Cross-references, not + silently fixed; new ratified symbols (σ*, L^{(q)}, [d,τ], K(β), χ_s, M ⊆ V×O) + enter the table in their own surgical PR. [INFERENCE — a notation refresh is its + own change; folding it in here would smuggle scope.] +7. **No external submission.** The register's venue park stands (dn-research-register, + Parked decisions). [ESTABLISHED.] +8. **The research Question stays owner-only.** This note names structures; it does not + author the study's Question. [ESTABLISHED — standing rule.] +9. **Nothing is restated that lives elsewhere.** Proofs live in the ratified notes and + their fable-pass capsules; enforcement lives in tests; formal statements will live + in `formal/`; the ledger and this note index and cite. [ESTABLISHED — DRY is a + defect, not a nit.] +10. **No `core/` code changes are licensed.** MF-2/MF-3 write tests only; a defect a + new falsifier exposes lands as a `type:defect` issue, never a drive-by fix. + [INFERENCE — a falsifier batch and a behavior change never share a plan.] + +### 1.3 The sibling boundary — pointing back + +The warrant capsule carries two arcs; the sibling (dn-research-register) is the +register arc and this note is the foundations arc. The shared boundary, honored from +this side: the claim-ladder labels of its §2.3 are *consumed* here — every ledger row +lands as a labeled claim with a falsifier, in the sibling's vocabulary, and neither +note redefines the labels without the other. The float-epsilon caveat appears in both +homes as designed: there as a register rule (its §2.3.3/R7), here as substance +(§2.5). And the sibling's parked Lean row is re-pointed at this note's ladder by the +surgical edits riding this same PR: default **L0 — ladder specified here (§2.4)**; +re-entry for L1, **the laws ledger's first laws exist to state** (issue #48's own +proposed wording, applied under owner seed 3's direction). + +## 2. Principles / decision + +### 2.1 The frame — correctness is structure-instantiation, not axiomatic descent + +**Decision.** The palace's foundation is the discipline that each mathematical +component (a) **names the known structure it is a model of**, (b) **states the +hypotheses** under which it instantiates that structure, and (c) **imports that +structure's theorems** only under those hypotheses. "Model of a known structure" is +the sibling's own lexicon row for structure-instantiation; the register note carries +the term, this note makes it the load-bearing frame. + +Why this and not first principles: the mathematics is **finite in substance**. The +Laplacian family is finite real symmetric matrices (`core/kernel/complex/laplacian.py` +— L, L_sym under w ≥ 0, L̄ via its signed identity: PSD quadratic forms on finite +weighted graphs, each under its stated hypothesis); the built +curvature is integer combinatorics on finite supports (`core/kernel/complex/curvature.py` +— Forman, exact over ℤ; the finite-LP object is the *deferred* Ollivier enrichment, +not the floor, §2.3.3); memberships are a finite coordinate-keyed relation +(`core/stores/memberships.py`, §2.3.1); embeddings are finite-dimensional +inner-product spaces; the temporal operators are finite-matrix operator algebra +(dn-temporal-retrieval-algebra). Reliance sits far below ZFC — finite sets, finite +linear algebra, elementary order theory and probability. Deriving these "from first +principles" would add no power the finite structures do not already give; what *does* +add power is the transfer of theorems: when the hypotheses hold, the structure's +results hold for free — and the hypotheses do real work. Mathlib's +components-equal-nullity theorem (a `SimpleGraph.lapMatrix` result — **unweighted**) +is the proof *substrate* for `spectral.py`'s per-component contract (issue #48); +binding it to the palace's **weighted** L takes one short house step (w ≥ 0; the +kernel reduces to the unweighted support graph's), stated on the LAP rows and priced +into MF-4. + +**The bridges — the working correspondences.** Owner seed 1 asks whether foundational +math is "the bridge to other branches — our mini Langlands". The honest answer: the +Langlands analogy lands not as a program but as the correspondences the palace has +already implemented *between* its structures. (The metaphor stays internal per the +sibling's R5 — never in external register.) The implemented bridges, each cited to +its home and restated nowhere: + +| bridge | the correspondence, one clause | home | +|---|---|---| +| graph ↔ operator | weighted σ-graph ↔ L = D − A, the two-point L⁺ form R_eff, the heat kernel e^{−tL} | core/kernel/complex/laplacian.py; core/graph/conductance.py (CN-3/CN-4; P3/P4) | +| direction ↔ gauge | direction/sign data ↔ the magnetic fibers L^{(q)}; flux = abelianized holonomy; L̄ = the q=1/2 fiber | dn-magnetic-laplacian (design-only; q=0 built) | +| curvature ↔ transport | support combinatorics ↔ the Forman floor (built, exact ℤ); the OT side (Ollivier over W₁) deferred, PD-c | core/kernel/complex/curvature.py (§2.3.3) | +| membership ↔ keyed relation | occupancy ↔ keyed partial function; multiset atom projection; Boolean support image | memberships.py; dn-vector-membership-store §4 (§2.3.1) | +| time ↔ operator algebra | supersession ↔ π_active/σ_* transport, 𝔸 = d + τ, the dilation of T_active | dn-temporal-retrieval-algebra A1–A8 (§2.3.2) | +| query ↔ semiring / kernel cone | retrieval modes ↔ one K(β) deformation: tropical (min,+) ↔ heat kernel ↔ Gram | dn-core-query-protocol §2.2 (§2.3.2) | + +Each row is a correspondence between two named structures, already load-bearing in +ratified text or shipped code. The frame's obligation is that every future +mathematical component adds its row — or says honestly that it has no structure to +name yet, which is a **Conjecture**-labeled row, not an absent one. + +### 2.2 The laws ledger — one index that makes honesty visible + +**Home and form.** `docs/LAWS.md` — a single authored artifact (verified absent at +HEAD; minted by MF-1). Not derived, not a skill, not per-module scatter: one file the +owner can read top to bottom, the `docs/lexicon.md` precedent from the sibling. Every +module docstring that carries an OBJECT/INVARIANT/ENFORCED header keeps it — the +ledger indexes those headers, it does not replace them. + +**The row schema — seven columns, all mandatory.** + +| column | carries | +|---|---| +| law id | family-prefixed: MEM-, LAP-, SPC-, CUT-, CND-, CRV- + number | +| statement | the law, one clause, **with its arithmetic domain** (exact ℤ/ℚ, or ε = over float64) — the §2.5 discipline | +| claimed structure | the known structure the law instantiates (§2.3's namings; standard names per the sibling's R5) | +| code anchor | file + defining symbol (`module.py::name`), resolved at HEAD; line numbers are gloss, never the key | +| ladder label | the sibling's §2.3.1 rung — consumed, never redefined | +| falsifier | the pytest node id (`file::test_name`) that would catch the law false — or `GAP`, which caps the label | +| formal status | the `formal/` statement/proof ref (§2.4) — or `—`; at seeding, uniformly `—` (no `.lean` exists at HEAD) | + +**The single-sourcing discipline, stated as law.** The ledger *indexes*: proofs live +in the ratified notes and their capsules (cited by id), enforcement lives in the named +tests, formal statements live in `formal/`. The ledger never restates any of them — a +ledger row that carries a derivation is a defect. This is what keeps thirty rows +honest instead of thirty opportunities to drift. + +**Resolution and repair, stated once.** Anchors resolve **at HEAD**: the MF-2 checker +asserts each anchored symbol exists and each falsifier node id is collected by +pytest. When a refactor moves a law's ground, the checker reds and **the refactoring +PR carries the row repair** — detection is mechanical, repair rides the PR that moved +the code. No standing sweep, no per-PR read-through duty; what the minimal checker +cannot see (statement drift against unmoved symbols) stays honestly parked (Parked +decisions). + +**The label discipline, inherited.** Per the sibling's §2.3.2 item 3, each law lands +as a labeled claim — typically Claim, or Proposition with its paired falsifier — one +falsifier per law. The consequences this note adds as ledger policy: **a law whose +falsifier column reads `GAP` is at most Conjecture** — the falsifier described, not +yet run — matching the register's ceiling (a Claim requires its *named* falsifier; +seed cells write the target, e.g. `Conjecture → Prop at MF-2`). Two ledger-side +**annotations** qualify a rung without minting one: *(cited)* — a documented-only +theorem citation, never more than the rung it decorates; *(structural)* — a law +enforced by a structural scan rather than a numeric assertion. A **Proposition** row +bears its label at the law's home artifact: the checkable inline proof lives in the +home note, docstring, or test derivation, the statement cell cites that home, and +the ledger mirrors — never houses — the proof (single-sourcing). The ledger exists +precisely to make those caps visible instead of buried in docstrings. + +**The seed inventory.** MF-1 seeds the ledger from the tables below — real laws, real +anchors, grounded at HEAD `68d8d39` plus the staged memberships store (the bp-152 lineage — +the vector-membership-store build plan; staged == worktree, verified). These tables are the graduation spec, terse +by design (anchors here are draft start-lines — **MF-1 composes them into symbol +anchors and pytest node ids per the schema**, lines demoted to gloss; statements +compressed; the ledger's structure and formal-status columns are composed at MF-1 +from §2.3 and `—`): once MF-1 merges, the +ledger is authoritative and these tables are provenance. `GAP → MF-n` marks the +enforcement gaps §2.6 prices. Memberships first — the one family whose laws hold +exactly over ℤ, end to end. + +**I. Memberships** (`core/stores/memberships.py`, staged; tests +`tests/unit/test_memberships.py`, staged — the house falsifier discipline at its most +developed): + +| id | law (arithmetic domain) | anchor | label | falsifier | +|---|---|---|---|---| +| MEM-1 | keyed finite relation; atom projection a multiset; n_doc ≤ n_occ (exact, ℤ) | memberships.py:148 | Definition + Proposition | test_memberships.py:204 (two-rows witness) | +| MEM-2 | version fibers partition M: Σ\|fiber\| = \|M\| (exact, ℤ) | memberships.py:264 | Proposition | test_memberships.py:633 (seeded violating subclass) | +| MEM-3 | slot runs = adjacent-collapse RLE; \|edges\| = \|runs\|−1; a revert stays visible (exact, ℤ) | memberships.py:381 | Proposition + Claim | test_memberships.py:588 | +| MEM-4 | re-land is idempotent BY reconciliation, never by short-circuit — the C1 law (exact, ℤ) | memberships.py:243 | Claim | test_memberships.py:286 (exhibited wrong lander) | +| MEM-5 | currency selects one fiber per path; current_any(v) ⇔ n_doc(v,t) > 0 (exact, ℤ/Bool) | memberships.py:294 | Claim | test_memberships.py:653 (seeded drift flip) | +| MEM-6 | \|V\| monotone up; purge the one logged decrement — tombstones M, never deletes (exact, ℤ) | memberships.py:511 | Claim | test_memberships.py:671; :440 (the hole exists) | +| MEM-7 | chain fibers ⊆ version fibers, ⊊ iff an off-chain fiber exists (witnessed); side-branch atoms on no run (exact, ℤ) | memberships.py:392 | Claim | test_memberships.py:614 | +| MEM-8 | presence is typed by geometry: keyed (content_id) × (model, dim) (exact, strings) | memberships.py:191 | Claim | test_memberships.py:310 (same-embedder control) | +| MEM-9 | coverage(atom) ⊆ span(slot); strict for nested symbols; shell span = whole file (exact, ℤ) | memberships.py:94 | Proposition + Claim | test_memberships.py:147 (leaf control) | +| MEM-10 | crash orphans observable, invisible to default search; re-land adopts at zero embeds (exact, ℤ/Bool) | memberships.py:432 | Claim | test_memberships.py:479 (injection asserted) | +| MEM-11 | the kernel never imports the store; memberships enter as data (RowSource) | memberships.py:9 | Claim (structural) | test_memberships.py:228 (negative control) | + +**II. Laplacian & balance** (`core/kernel/complex/laplacian.py`, `balance.py`) **and +spectral** (`core/complex/spectral.py`): + +| id | law (arithmetic domain) | anchor | label | falsifier | +|---|---|---|---|---| +| LAP-1 | L·1 = 0 for L = D − A (exact weights: exact; f64: allclose 1e-8; route agreement ≤ 4·eps·max) | laplacian.py:26 | Proposition | test_complex.py:100; test_graph_boundary.py:69 | +| LAP-2 | xᵀLx = Σ w(x_u−x_v)² ≥ 0 (symmetric A, w ≥ 0); L̄ PSD via its signed identity (laplacian.py:52) | laplacian.py:1 | Conjecture → Prop at MF-2 | GAP — direct PSD untested | +| LAP-3 | dim ker L = #components (w > 0 on edges; SimpleGraph thm in Mathlib, weighted via support) | laplacian.py:27 | Conjecture (cited) | GAP — nullity never counted → MF-2 | +| LAP-4 | Spec(L_sym) ⊆ [0,2] (A ≥ 0); D^{−1/2} := 0 at degree 0 (ε = 1e-9, float64) | laplacian.py:33 | Proposition + Definition | test_complex.py:104; convention pointwise → MF-2 | +| LAP-5 | λ_min(L̄) = 0 ⇔ balanced (Hou/Kunegis); house reading: max over components (ε = 1e-6) | balance.py:28 | Claim (cited) | test_complex_properties.py:93 (converse: one instance) | +| LAP-6 | a triangle is frustrated ⇔ it carries an odd count of negative edges (exact, ℤ/2 parity) | balance.py:9 | Proposition | test_complex_properties.py:96 | +| SPC-1 | clustering is deterministic (fixed ramp v0, seed 0); ≥90% stable at 1e-3 noise (float64, platform-scoped) | spectral.py:32 | Hypothesis | test_complex_properties.py:35, :66 | +| SPC-2 | components are clustered independently, never merged (labels disjoint — exact, sets) | spectral.py:119 | Conjecture → Claim at MF-2 | GAP — behavioral only (test_complex.py:108) | + +**III. Cut & conductance** (`core/complex/cut.py`; `core/graph/conductance.py`): + +| id | law (arithmetic domain) | anchor | label | falsifier | +|---|---|---|---|---| +| CUT-1 | Φ(S) = w(∂S)/min(vol S, vol S̄) ∈ [0,1]; degenerate S → 0.0, no community → 1.0 — OPPOSITE alarms (float64) | cut.py:35 | Definition + Conjecture → Prop at MF-3 | GAP — untested | +| CUT-2 | Cheeger ½λ₂ ≤ h ≤ √(2λ₂), λ₂ of L_sym; h = min over ALL cuts (partition min bounds it above); computed nowhere | cut.py:7 | Remark | none owed — nothing depends on it | +| CUT-3 | grounding_cut = integer max-flow; monotone in capacities; chain bottleneck (dyadic ℚ, ×2¹⁰) | cut.py:70 | Prop. (cites max-flow min-cut) | test_structural_interpreters.py:88 | +| CND-1 | R_eff = L⁺ᵢᵢ + L⁺ⱼⱼ − 2L⁺ᵢⱼ per component; ∞ across components (rtol 1e-10; ∞ exact) | conductance.py:226 | Definition + Claim | test_conductance.py:206; graph_boundary:125 | +| CND-2 | a rise requires a weight-increased edge (Rayleigh, cited; ε = 1e-9); attribution = leave-one-out | conductance.py:441 | Claim (cited) | test_conductance.py:124; quality suite | +| CND-3 | every profile carries degeneracy diag corr(R_eff, 1/d_A + 1/d_B); ≥ 0.9 flips authority to finite-t (float64) | conductance.py:256 | Claim | test_conductance.py:150 | +| CND-4 | d_t² = Σ e^{−2tλ_k}(φ_k[i] − φ_k[j])² over the COMBINATORIAL L; a reading = the (σ×t) grid (f64) | conductance.py:239 | Proposition + Definition | test_conductance.py:163 | +| CND-5 | w = cos^α·exp(s_lat·a_lat − s_seq·a_seq); signs are law; magnitudes ship 0 ⇒ w = cos (IEEE-exact) | conductance.py:106 | Definition + Claim | test_conductance.py:260 (AST scan) | +| CND-6 | χ_s = chain/N_s ∈ (0,1] for window=None (the only wired call); None at N_s=0 (ℚ-valued, 1 f64 div) | conductance.py:375 | Proposition | test_conductance.py:314; windowed → MF-3 | + +**IV. Curvature** (`core/kernel/complex/curvature.py` — Forman, not Ollivier; §2.3.3): + +| id | law (arithmetic domain) | anchor | label | falsifier | +|---|---|---|---|---| +| CRV-1 | Ric_F = 4 − deg(u) − deg(v) + 3·\|△(u,v)\| on binarized support (exact, ℤ); the declared augmented-Forman variant | curvature.py:25 | Definition | exactness exercised by CRV-2 | +| CRV-2 | two m-cliques + one bridge: Ric_F(bridge) = 4 − 2m, the strict unique minimum (exact, ℤ) | test_structural_interpreters.py:26 | Proposition | its own paired property test | +| CRV-3 | most_negative_edges: κ ≤ 0 else argmin; (κ,i,j) tie-break; top_k cap (κ int-valued f64, == exact) | curvature.py:46 | Definition | GAP — untested (consumer: dreaming) → MF-3 | +| CRV-4 | Ollivier–Ricci over W₁ deliberately absent — Forman is the floor (issue #48: Mathlib lacks OT) | curvature.py:15 | Observation | the absence is stated in-code | + +The property-test substrate is existing house practice, not a proposal: `hypothesis` +is already a dev dependency with a `tests/property/` tier, and +`docs/WHITEPAPER-FORMAL-PROPERTIES.md` already defines a per-invariant discharge +scheme. **The catalog boundary, stated once:** the whitepaper's I-rows are +architecture invariants and stay its own; `docs/LAWS.md` owns algebraic laws; the +§A.5 family-5 obligations the whitepaper delegates to the REASONING-COMPLEX +companions are absorbed here as rows, and the H-N ids those companions and test +docstrings already carry (H4/H5/H6 …) are cross-referenced in the row statements — +MEM-/LAP-/SPC-/CUT-/CND-/CRV- become the per-law coordinates going forward. §A.5's +own staleness (it still says `core/complex/` "does not exist yet") is flagged here +exactly as NOTATION.md's is, into the same parked refresh lane. The ledger extends +the tiering; it does not invent a parallel one. + +### 2.3 Structure honesty — naming what is actually instantiated + +#### 2.3.1 Memberships — the true structure, settled + +The capture capsule (PR #42) says "memberships form a finite Boolean algebra." The +implemented store says otherwise, in its own header: `core/stores/memberships.py:5` — +*"INVARIANT: MULTISET, never a set."* This note resolves the tension on the record's +side, and sharpens it, because "a multiset" is itself lossy about what is built: + +**Definition (the structure as coded).** The membership relation M is a **finite +partial function on coordinate space** — the SQLite primary key +`(path, blob_sha, layer, chunk_index)` makes each row unique by *occupancy +coordinates*, with `content_id` outside the key. Three derived layers, each real: + +- **Version fibers are finite sequences.** Each fiber M(path, blob_sha) is totally + ordered by `chunk_index` and read back in that order — a *word* over the atom + alphabet, not a bare bag (`memberships.py:264`; order asserted by + `test_memberships.py:133`). Held-by-whom, said plainly: the PK enforces uniqueness + per (path, blob_sha, *layer*, chunk_index); fiber-wide total order and + one-current-fiber-per-path are the **writer's** invariants (the pure derivation; + `reconcile_currency`'s postcondition) — stated hypotheses for any L1 statement, + not schema constraints. +- **The atom projection is a multiset.** Pushing rows along π: row ↦ content_id gives + the free-commutative-monoid reading: n_occ(v) = multiplicity (row count), and the + coarser path pushforward gives n_doc(v) = document frequency; n_doc ≤ n_occ, strict + on the enforced duplicate-window witness (MEM-1). Two byte-identical windows are two + rows — the schema-enforced counterexample to any set reading. +- **Boolean structure appears exactly once: the support image.** The current-view + predicate current_any(v) ⇔ n_doc(v,t) > 0 maps into 𝒫(atoms), and the query-visible + read `currently_held` returns exactly that support set — **Observation:** the + *image* of the support map lives in a finite Boolean algebra of subsets. + (`known_atoms` is a different surface: the embedder-typed atoms-ledger read — + MEM-8's relation — which includes zero-occupancy crash orphans, so it is *not* + the support image.) That is a fact + about the image, not about the store: no store operation is claimed to respect + Boolean structure (land/purge are not ∨/∧-homomorphisms on views). Any stronger + reading — Boolean-algebra laws holding for the view under the store's dynamics — is + **Conjecture**, unheld and untested; its falsifier, named at birth per the ladder: + a view-level ∨-homomorphism check across a land/purge pair (nothing claims it + commutes). The capsule's sentence, per the ladder, is + refuted as a statement about occupancies and demoted to that Conjecture about the + current-view image. + +The laws the structure carries are the MEM rows of §2.2 — fiber idempotence held *by +reconciliation* rather than by skipping (MEM-4, the C1 law, with the wrong lander +exhibited in a mutation test), purge-tombstone monotonicity (MEM-6), and +currency-as-cache coherence (MEM-5) chief among them. The domain claim worth its own +sentence: **the memberships family is pure ℤ/Boolean/string — zero floats — so every +one of its ledger rows may claim "holds exactly," with no ε anywhere.** It is the one +component where exactness is fully real, which is why it seeds first. + +#### 2.3.2 The temporal and query algebras — pinned vs. conjectural + +What is **pinned**, by ratified text (cited, never restated here): +dn-temporal-retrieval-algebra (the temporal-retrieval algebra) pins the two mode-3 +operators and their non-interchangeability (π_active a contraction and not a chain +map; σ_* a chain map), Theorem A1's K(β) family with its two endpoints and the +convergence identity, the six A3 results (the [d,τ] severed-citation support formula, +𝔸² = [d,τ] + τ², the dilation reading, the owner-as-only-energy-source contraction), +A7's apophenia discriminator, and A8's β* finiteness criterion. +dn-core-query-protocol §2.2 pins the query-mode algebra: modes 1a/1b/2/3, the +tropical-to-heat-kernel deformation via Maslov dequantization, the PSD-kernel cone +operations, Moore–Aronszajn (not Mercer) as the mode-2 warrant. + +What remains **conjectural or open**, honestly: the diamond/τ²-coherence closure +(TA-c) is a *sketch* by the ratified note's own grading — and dn-magnetic-laplacian +refuted its abelian-closure form three ways; the TA-a..e and PD-a/b/c parks (their notes' own parked-decision ledgers) stand, +re-entered only through their own named gates. This note reopens none of them. + +The register-honesty caveat this note adds: those ratified results are +prose-proof-warranted (the fable-pass capsules, cited by their notes) and their +labels are merged provenance — this note relabels nothing. What the ledger records is +the *formal* column: uniformly `—` today, honestly. The L1/L2 rungs (§2.4) target the +finite/algebraic core first (memberships, Laplacian PSD/nullity, L⁺ symmetry); the +temporal algebra's analytic results are not first-batch material and are not promised. + +#### 2.3.3 Curvature — Forman is the floor + +**Observation.** The implemented curvature is the *augmented Forman–Ricci* variant on +the binarized support — pure degree-and-triangle combinatorics, integer-valued, no +optimization anywhere (`core/kernel/complex/curvature.py:25`, CRV-1). Ollivier–Ricci +over W₁ is *deliberately not implemented* (`curvature.py:15`) — it is the parked PD-c +enrichment, and the finite Kantorovich LP enters the palace only when that park +re-enters. Two corrections ride this naming, neither weakening a verified status: +the capsule's "curvature = finite LP" describes the deferred enrichment, not the +shipped floor; and the Lean report's Axis-A gloss of `curvature.py` as +"Ollivier-Ricci over W₁" is a loose *target description* — its Mathlib-absence +verdicts for Ollivier and Cheeger stand exactly as verified (issue #48). The ledger +anchors house curvature on Forman (CRV-1/2/3) and carries the OT side as the honest +absence (CRV-4). + +### 2.4 The Lean ladder — L0–L4 adopted as design + +**Decision.** The four-rung adoption ladder proposed by the Lean investigation +(issue #48 — Mathlib coverage, Plausible, FloatSpec, lean-action, and the agent-era +cost premise all verified there 2026-08-09; this note cites and does not re-verify) +is adopted as design. The investigation's own boundary holds: the ladder is +foundations-arc substance, so it lands here, and the sibling's parked row now points +at this section (§1.3). + +- **L0 — today.** Nothing. No `.lean` exists in the repo (verified at HEAD). The + ladder's default resting state, and where it retracts to if L1 fails its falsifier. +- **L1 — statements as specs** (licensed: MF-4). `formal/` — a sibling lake package + with **zero import coupling with `core/` in either direction** (non-goal 1): + `lakefile` + pinned `lean-toolchain`, Mathlib as the dependency, cache via + `lake exe cache get`. Lean *statements* of the first ledgered laws — the memberships + relation/multiset laws (MEM-1/2/3/5), L PSD and **L·1 = 0 for the combinatorial L** + (the report's bundling corrected: zero row sums is a law of L, not of L_sym, whose + kernel vector is D^{1/2}·1), L_sym PSD, L⁺ symmetry/PSD — each carrying a + **Plausible counterexample attack** (the falsifiers-before-proofs epistemology as a + Lean tactic). Proofs taken where Mathlib gives them directly: the named `SimpleGraph.lapMatrix` + lemmas (`isPosSemidef_lapMatrix`, components-equal-nullity — issue #48) discharge + the **binarized-support** statements in one line, and the weighted forms take the + small house reduction lemma (w ≥ 0 — priced here, not free); `sorry` elsewhere. **The sorry-count ratchet — review-enforced in the advisory era, machine-enforced + at the flip:** `formal/sorry-budget` records one integer; the CI job (MF-5) counts + `sorry` occurrences after `lake build`, fails when count > budget, and **asserts + the axiom escape shut** (`axiom`/`admit` grepped to zero outside Mathlib — every + declaration rests on Lean's three standard axioms alone); a diff that raises the + budget, lowers the count by deleting or weakening statements, or swaps `sorry` for + an axiom is the defect MFF-3 names. Every formal statement carries + its ledger law id in a comment, and the ledger's formal column points back — the + two-sided cross-reference MFF-4 patrols. +- **L2 — proofs of the finite/algebraic core** (licensed with entry condition: MF-6). + Discharge L1 obligations over exact arithmetic, agent-authored under supervision — + the mathematician-directs-AI workflow the investigation verified at + research scale (arXiv:2607.08986: headline theorems in about a week, the full + 299-declaration development in about a month), applied at palace scale. This + unlocks the sibling's Theorem rung honestly: **Theorem (machine-checked, + `formal/...`)** — reachable without lowering its price. +- **L3 — the numerical bridge.** FloatSpec-style float-ε models, entered **per-claim + only**, where a design claim demands a machine-checked ε-bound. Parked with + re-entry (Parked decisions); not licensed (non-goal 2). +- **L4 — verified kernels.** Parked. No palace claim needs it (issue #48). + +**The bridge stays two-sided.** Lean never proves the NumPy (issue #48 Axis B): Lean +states and proves laws over exact arithmetic; Hypothesis property-tests the Python +against the same laws with tolerance bounds; the artifacts cross-reference by law id. +One law, two independent attack surfaces — the ledger is the join. + +**CI, advisory before required.** MF-5 wires `lean-action` (elan install, +`lake build`, Mathlib cache) as an **advisory** job. The flip to required is the +owner's hand alone, after a stated stability window: the advisory job green on every +merge for four consecutive weeks with no fix-forward commit targeting `formal/` +breakage. Until then a red lean job blocks nothing — it informs. + +**The rung falsifier, carried verbatim in force** (issue #48): if the statement layer +never catches a mis-stated law that Hypothesis alone missed, by the third law batch, +L1 is decoration and retracts to L0 — MFF-5, and the un-minted rungs above it die +with it. + +### 2.5 Float-epsilon as substance — the three arithmetic tiers + +The sibling's rule (its §2.3.3 and R7): every algebraic or equality claim states its +arithmetic domain, because float addition is non-associative and exact-equality claims +over floats are precision theater. Consumed here as **mandatory ledger schema** — the +statement column carries the domain or the row is malformed. The substance this note +adds is that the codebase already practices three separable tiers, which the ledger +names per row: + +1. **Exact domains — where equality is real.** Memberships (pure ℤ/Bool/string, zero + floats); Forman curvature (integer closed forms asserted with `==` — sound + *because* integer-valued); grounding_cut (integer capacities + fixed-point ×2¹⁰ = 1024, so flow values are dyadic rationals exactly representable + in float64 — the one deliberate escape from float arithmetic). Exact-equality + claims are licensed here and only here. +2. **Ulp-classed reassociation — where float error is bounded by construction.** The + `test_graph_boundary.py` doctrine, adopted as the ledger's model entry (LAP-1): + Laplacian off-diagonals exact, degree sums within 4·eps·max — with the written + rule that reassociation is not a metric change and O(1) divergence is a P4 stop; + R_eff route-invariance at rtol 1e-10, "generous over ulp noise, catastrophically + failed by any real metric change." +3. **Named tolerance constants — where ε is doctrine.** 1e-6 (balance zero — + test-enforced in the property suite; `is_balanced` itself ships `tol=1e-8`), 1e-9 + (Rayleigh slack, spectrum bounds), 1e-12 (zero tests), 0.9 (degeneracy authority) + — deliberately segregated from tunable magnitudes (`conductance.py:159-160`: *"a + tolerance (module constant), not a tunable magnitude — it stays OUT of + `CONDUCTANCE_THRESH`"*; the :96 header comment states the same law). Ledger rows + cite the constant they are enforced at, naming the enforcing site when it differs + from the shipped default. + +χ_s sits deliberately *between* tiers, and its row says so: ℚ-valued in substance (a +ratio of small integers) but computed as one float64 true division +(`conductance.py:390`) — `= 1.0` and the `≤ 1` bound are exact comparisons (n/n = 1.0 +exactly; (n−1)/n rounds strictly below 1.0 for realistic N_s), general equality is +not, and its own falsifier asserts `pytest.approx` (test_conductance.py:329), never +`==`. (And the (0,1] range law is stated **for `window=None`** — the only wired call; +a windowed numerator counts full-stratum chains, so the bound there is a stated +hypothesis, recorded on CND-6 and closed at MF-3.) + +Hypothesis falsifiers are tolerance-bounded accordingly; a falsifier asserting exact +equality over a tier-2/3 quantity is itself a defect the ledger review catches. + +### 2.6 What the ledger surfaces first — the enforced-vs-documented gap + +The seeding's immediate yield is the gap list, priced into MF-2/MF-3: **PSD of L and +L̄** as direct assertions and **dim ker L = #components** (documented-only in Python +while machine-checked in Mathlib by name — simultaneously the weakest local +enforcement and the cheapest honest L1 statement, issue #48); **Φ(S)** and +`min_conductance` (no direct unit test — only downstream range assertions — while +carrying two *opposite-direction* degenerate conventions: degenerate S → 0.0 +"maximally sealed" vs. no qualifying community → 1.0 "healthy", both definitional, +neither tested); **most_negative_edges'** emission rule (consumed by dreaming, zero +direct tests); the **isolated-node convention** pointwise; **never-merge-components** +directly. Where Mathlib has the theorem and the local suite does not even count the +nullity, the honest order of work is: state the law in the ledger (MF-1), test it in +Python (MF-2/3), state it in Lean (MF-4), prove it (MF-6). + +## 3. Consequences + +**On the owner's merge of this note, and not before** — six graduation licenses, +session-sized, dependency-ordered, split at graduation, named **MF-N** (mathematical +foundations) per the sibling's unit-naming precedent (WF-N → RR-N → MF-N). All plans +land `proposed`; the owner's merge or instruction is the readiness signal. Dispatch +is serialized (the budget rule). + +- **MF-1 — the ledger seeded** (docs-only; entry: the bp-152 store merged — see + Sequencing). Deliverable: `docs/LAWS.md` minted with + the §2.2 schema and the full seed inventory (~30 rows, memberships family first, + riding the staged bp-152 store), every row complete — statement with domain, + structure from §2.3, anchor, label, falsifier-or-GAP, formal `—`; plus the track + manifest's DoD row check-off. Zero proofs, zero tests — seeding is naming and + labeling. Falsifier: a row missing its arithmetic domain or claiming a structure + §2.3 does not warrant; acceptance: file parses, reserved-words grep clean + (the sibling's §2.3.3 table). +- **MF-2 — the Laplacian/spectral falsifier batch.** Deliverable: named tests closing + the family's GAP rows (direct PSD of L and L̄; nullity = component count; the + isolated-node convention pointwise; never-merge directly), Hypothesis-generated + where a planted family exists; **plus the minimal ledger checker** — + `tests/unit/test_laws_ledger.py`, parsing `docs/LAWS.md` and asserting every + anchored symbol exists at HEAD and every falsifier node id is collected by pytest + (the structural-enforcement rule: the index is only real once a test proves its + pointers); the checker and the falsifier batch are separable surfaces — split at + graduation if one session cannot carry both. Green, or a counterexample recorded + and filed as a `type:defect` issue — a result, not a failure (non-goal 10: no + drive-by fixes). Ledger labels upgrade only as tests land. Unit falsifier: a + planted stale pointer the checker passes; or a new falsifier that cannot fail + (checked against a deliberately mutated implementation at review). +- **MF-3 — the cut/conductance/curvature falsifier batch.** Deliverable: direct Φ(S) + known-value tests plus both degenerate conventions and the singleton-skip; the + most_negative_edges emission rule (κ≤0-else-argmin, tie-break, cap); the CND-6 + windowed-law falsifier (the χ_s hypothesis, §2.5). Same acceptance shape and unit + falsifier as MF-2 (a test that cannot fail is the defect). Serialized after MF-2 + (both write the shared ledger). +- **MF-4 — `formal/` L1.** Deliverable per §2.4: the sibling lake package (lakefile, + pinned `lean-toolchain`, Mathlib dep), statements of the first ledgered laws with + Plausible attacks, one-line Mathlib proofs where free, `sorry` elsewhere, + `formal/sorry-budget` recorded as the ratchet baseline. Acceptance is local: + `lake build` green, attacks run. Depends on MF-1 (statements mirror stated laws). + The plan budgets the first Mathlib cache fetch (multi-GB wall clock) as a + stop-and-raise if unavailable. **The toolchain install is an owner hand-act before + dispatch** (verified absent on this machine): `elan` via its official installer or + `brew install elan-init`; the pinned `lean-toolchain` self-resolves on first + `lake build`. A machine mutation belongs to the owner, not a plan. **The natural + split line, pre-named:** (a) package skeleton + toolchain + cache + one + pipeline-proving law; (b) the memberships model (coordinate-keyed relation, + fibers-as-words, the RLE run structure — definitions, not transcription) + the + statement batch. Split there rather than mid-session. Unit falsifier: a merged + statement whose Plausible attack never ran, or one that fails `lake build`. +- **MF-5 — the advisory CI job.** Deliverable: `.github/workflows/` lean job via + `lean-action` with the Mathlib cache, the sorry-budget assertion, the axiom-escape + guard, and the ledger⇄formal law-id cross-reference grep (MFF-4's mechanical half), + **path-scoped to `formal/**`** plus a weekly cron for drift, advisory; acceptance: + green on a real PR touching `formal/` with the cache hitting. Unit falsifier: a + "green week" in which no run built a `formal/` change counts toward nothing — the + flip window's weeks are qualified by at least one `formal/`-building run. A deliberate split from + MF-4 (different zone, different failure surface — runner cache/minutes vs. local + build); folding them is legal only if one plan's write_scope honestly carries both + zones. +- **MF-6 — the first L2 discharge batch** (entry-gated, not mintable before its + condition). Entry: MF-4 landed and its statements have survived their Plausible + attacks. Deliverable: proof discharge of the memberships/Laplacian statement set + over exact arithmetic; the sorry budget strictly decreases **by named-law + discharge** (law ids are the acceptance; the count is only the trace); the first honest + *Theorem (machine-checked, `formal/...`)* citations become available to future + artifacts. Falsifier: MFF-3 (a gamed ratchet). + +**Priced, so the owner ratifies with the bill visible.** MF-1 is one docs session +(the RR-1 shape). MF-2/MF-3 are one test-writing session each — the falsifier +batches are the expensive honesty, and they may *file defects* rather than fix them. +MF-4 is the investigation's own sizing: one build-plan-sized unit, plus the one-time +Mathlib cache cost. MF-5 is small. MF-6 is the first genuinely new-currency spend +(agent proof sessions under supervision) and is entry-gated so it cannot start on an +unproven statement layer. Ladder rungs above it cost nothing until entered. + +**Explicitly NOT licensed:** L3 (per-claim entry only, parked) and L4 (parked); +Ollivier–Ricci or Cheeger formalization (non-goal 3); the required-in-CI flip (owner +act, after the stated window); any `core/` code change (non-goal 10); the NOTATION.md +refresh (non-goal 6); authoring the Question (non-goal 8); relicensing anything of +the sibling's (RR-1/2/3 are its own). + +## 4. Wiring & enablement + +**How it wires:** `docs/LAWS.md` (new, authored — the §2.2 schema; the one ledger +artifact); `tests/unit/test_laws_ledger.py` (MF-2 — the symbol/node-id checker that makes +*pointer* rot machine-visible at HEAD; statement drift stays parked, named); the family falsifier tests in `tests/unit/` +and `tests/property/` (MF-2/3 — running under the normal pytest gate, no new +runner); `formal/` (MF-4 — sibling lake package: `lakefile`, pinned +`lean-toolchain`, `formal/Palace/*.lean` statement modules carrying ledger law ids, +`formal/sorry-budget`; imported by nothing in `core/`, importing nothing from it); +`.github/workflows/` lean job (MF-5 — `lean-action`, Mathlib cache, sorry-budget +assertion, advisory); `docs/tracks/mathematical-foundations.md` (this PR — the MF +DoD rows). `scripts/board.py`: zero lines. `CLAUDE.md`: zero lines. No daemon +surface anywhere in this arc — `mind-palace deploy` is not involved. + +**What it takes to flip it on:** (a) MF-1 merges → the ledger is live on read; +(b) MF-2/MF-3 merge → the falsifiers and the ledger checker run on every CI pass — +live on first run, no switch; (c) MF-4 merges → `lake build` is runnable locally +(owner prerequisite: `elan` installed by hand — official installer or +`brew install elan-init`; first build fetches the Mathlib cache); +(d) MF-5 merges → the advisory job runs per PR — live on the next PR, no switch; +(e) the owner's only hand-acts: adjudicate the track coordinate at this note's +merge, install `elan` before MF-4 dispatch, merge each MF plan's PR, and — after +the four-green-weeks window (qualified weeks, MF-5) — flip the lean job from +advisory to required, by hand, if he chooses. + +## Parked decisions + +| decision | default recorded | re-entry condition | +|---|---|---| +| L3 — float-ε formal bridge | not entered; rung specified §2.4 | a design claim demands a machine-checked ε-bound (per-claim entry, one claim at a time) | +| L4 — verified kernels | parked | a palace claim needs a verified kernel; none does (issue #48) | +| Ollivier–Ricci formalization | not licensed; Forman is the floor (§2.3.3) | a design claim needs curvature *theorems*, or Mathlib gains OT/W₁ (the KR layer is the on-ramp) | +| Cheeger-in-Mathlib recheck | absent, verified 2026-08-09 (issue #48) | cheap periodic recheck at each MF-4+ session; or a claim comes to depend on the inequality (CUT-2 leaves Remark) | +| ledger checker beyond minimal | MF-2's anchor/test-id checker only | a stale row the checker passed (statement drift) — then statement-hash or deeper checking becomes a unit | +| required-in-CI flip for `formal/` | advisory | four consecutive green weeks, then the owner's hand — never an agent act | +| NOTATION.md + whitepaper §A.5 refresh | both stale texts flagged (Family-5; "does not exist yet"), not fixed | one surgical de-stale PR; new symbols enter NOTATION there | +| toolchain / Mathlib pin bump | pinned `lean-toolchain`; bumped only in MF-track sessions, never drive-by | an MF session needs a newer lemma, or the advisory job reds on cache drift | + +## Falsifiers — what would prove this design wrong + +The owner ratifies falsifiers, not proofs. + +- **MFF-1 (ledger-rot):** a merged ledger row's anchor or falsifier name goes stale + and both review and the MF-2 checker miss it. The index then misleads — worse than + no index. Two occurrences reopen the checker park at the deeper tier. +- **MFF-2 (structure-mislabel):** a ledger row names a structure the code demonstrably + does not instantiate — the Boolean-algebra case is the template — and it merges + without a Conjecture cap. The §2.3 honesty discipline then failed at review, and + the row's whole column is suspect until re-audited. +- **MFF-3 (the ratchet gamed):** the sorry count drops by deleting or weakening + statements or by `axiom`/`admit` substitution rather than proof; or the budget file + is raised without a warranted note in the PR body; or padding statements are added + only to be "discharged." The ratchet then measures nothing; MF-6 cannot claim + discharge on it — its acceptance is named-law discharge, never raw count decrease. +- **MFF-4 (formal/ divergence):** a `formal/` statement and its ledger row drift — + the law id cross-reference broken or the statements semantically different — and + merge that way. The two-sided bridge (§2.4) is then one-sided decoration. +- **MFF-5 (the L1 value falsifier, issue #48's own):** by the third law batch the + statement layer has caught no mis-stated law that Hypothesis alone missed. L1 is + then decoration: it retracts to L0, MF-6 is never minted, and the parked rungs stay + parked — the ladder dies at its first rung, honestly. + +## Cross-references + +Code, at `68d8d39` plus the staged store (paths current at HEAD — several ratified +notes pin pre-migration `core/complex/` paths for what now lives under +`core/kernel/complex/`; content stands, cite by object and current path): +`core/kernel/complex/laplacian.py` (L, L_sym, L̄ — LAP rows), +`core/kernel/complex/balance.py` (signed spectrum, masking fix), +`core/kernel/complex/curvature.py` (Forman floor; Ollivier deferred — CRV rows), +`core/complex/spectral.py` (SPC rows), `core/complex/cut.py` (CUT rows), +`core/graph/conductance.py` (CND rows; the OBJECT/INVARIANT/ENFORCED header and +cite-don't-restate docstring pattern the ledger indexes), +`core/stores/memberships.py` + `tests/unit/test_memberships.py` (staged — MEM rows; +the precondition-first falsifier discipline), `tests/unit/test_graph_boundary.py` +(the float-ε model entry), `tests/property/` + `docs/WHITEPAPER-FORMAL-PROPERTIES.md` +(the existing discharge tier this note extends), `pyproject.toml` (hypothesis already +a dev dependency). + +Artifacts, glossed: `docs/brainstorms/mathematical-foundations.md` (the warrant +capsule, PR #42, sequenced first — owner seed 1, structure-instantiation, +falsifiers-before-proofs, the float-ε risk; its "finite Boolean algebra" and +"curvature = finite LP" phrasings are corrected by §2.3.1/§2.3.3 on the record's +side); `docs/design-notes/dn-research-register.md` (the sibling, same PR — the claim +ladder §2.3, reserved words, R5/R7, the §1.3 boundary; its parked Lean row re-pointed +at §2.4 here by this PR's surgical edits); GitHub issue #48 (the Lean investigation — +Mathlib coverage table, Plausible/FloatSpec/lean-action, the agent-era cost premise, +the L0–L4 proposal; external claims verified there 2026-08-09 *unless marked +otherwise in the report* — every claim this note leans on is a VERIFIED row, the one +[FROM MEMORY] row (semiring/inner-product bedrock) is not load-bearing here — cited, +never re-verified); `docs/design-notes/connectivity-instruments.md` +(dn-connectivity-instruments, ratified — CN-1..CN-7); +`docs/design-notes/core-graph-instruments.md` (dn-core-graph-instruments, ratified — +P1/P3/P4, the import-walk tooth); `docs/design-notes/magnetic-laplacian.md` +(dn-magnetic-laplacian, ratified, design-only — the L^{(q)} family, F1–F5); +`docs/design-notes/temporal-retrieval-algebra.md` (dn-temporal-retrieval-algebra, +ratified — A1–A8; its banner predates the merge-gated regime and is not quoted as +live mechanics); `docs/design-notes/core-query-protocol.md` (dn-core-query-protocol, +ratified — §2.2 the query-mode algebra); `docs/design-notes/vector-membership-store.md` +(dn-vector-membership-store — in force by owner merges; its frontmatter `status: +draft` is provenance, never edited); `docs/design-notes/fiber-geometry.md` +(dn-fiber-geometry, ratified — FG-0/FG-5); `docs/NOTATION.md` (the symbol authority — +**staleness flagged, not fixed:** its Family-5 header still says `core/complex/` +"does not exist yet", false at HEAD; the refresh is parked, non-goal 6); +`docs/tracks/mathematical-foundations.md` (this note's manifest, minted in this PR — +⚑ owner adjudicates the coordinate at the merge). diff --git a/docs/design-notes/dn-research-register.md b/docs/design-notes/dn-research-register.md index a8b66b3..ad7207a 100644 --- a/docs/design-notes/dn-research-register.md +++ b/docs/design-notes/dn-research-register.md @@ -16,6 +16,7 @@ links: - docs/book/preamble.tex # the house claim registry + citation macros the paper format factors and extends - .claude/skills/book/SKILL.md # LaTeX conventions authority — reused, not forked - .claude/skills/issue/SKILL.md # the label taxonomy the claim ladder maps onto + - docs/design-notes/dn-mathematical-foundations.md # THE SIBLING — same PR #47; consumes the §2.3 labels; carries the laws ledger (docs/LAWS.md) + the Lean L0–L4 ladder supersedes: null # PARTIAL overlay on dn-track-board-and-deskcheck-gate D3 — template/body shape only (§2.4); D3's pre-regime verdict-hook mechanics are not propagated; D2's board, the dc- lifecycle, and the queue are untouched superseded_by: null warrant: docs/brainstorms/mathematical-foundations.md # owner seed 2, 2026-08-09 — quoted in the opening blockquote; reaches main via PR #42, sequenced first @@ -103,11 +104,13 @@ DoD rows that make this work visible to the lane's own deskcheck. 5. **The research Question is not authored here.** Study-not-product: the Question is owner-only. This note builds the slot and leaves it empty, labeled empty. [ESTABLISHED — owner-only authorship is a standing rule.] -6. **Lean / proof-assistant adoption stays parked.** Re-entry unchanged from the - warrant capsule: a claim a property test cannot falsify. Consequence for the ladder: - "Theorem" is expected to be rare-to-absent, and its absence is honest (§2.3). - [ESTABLISHED once the warrant lands — the capsule park, restated not reopened; the - capsule is this note's warrant and is sequenced first (PR #42, see Sequencing).] +6. **Lean adoption is not decided here — the sibling carries it.** The warrant + capsule's flat park is superseded by the L0–L4 ladder of + dn-mathematical-foundations (§2.4 there; investigation: issue #48). Consequence + for the ladder unchanged in spirit: "Theorem" stays rare until L2 discharge makes + *Theorem (machine-checked, `formal/...`)* honestly reachable, and its absence + meanwhile is honest (§2.3). + [ESTABLISHED — the park's disposition moved to the sibling, riding this same PR.] 7. **No second LaTeX stack.** The paper format factors the book's preamble and extends its notation registry; it duplicates nothing. Two copies drift. [ESTABLISHED — DRY is a defect, not a nit.] @@ -118,20 +121,22 @@ DoD rows that make this work visible to the lane's own deskcheck. [INFERENCE — "evolved, never paralleled" is this note's reading of the owner's seed against the regime's retirement of ceremony; the owner confirms at ratification.] 9. **The laws-ledger sweep is not licensed here.** The per-component - claimed-structure + laws + falsifier sweep belongs to the sibling mathematical- - foundations arc (§1.3); this note only specifies the labels that sweep will consume. - [INFERENCE — sibling boundary drawn so neither arc balloons.] + claimed-structure + laws + falsifier sweep belongs to the sibling, + dn-mathematical-foundations (§1.3 — same PR); this note only specifies the labels + that sweep consumes. [ESTABLISHED — the boundary is owner-directed (seed 3, + 2026-08-09) and both notes ride PR #47.] 10. **The dormant deskcheck-gate machinery is not retired here.** `gate-guard.sh`, `_lib.py`'s verdict clauses, and `tests/integration/test_deskcheck_gate.py` stay untouched; the carrier keeps their expected shape so they stay green. Disposition is parked, and filed as a `parked` issue with this PR so it cannot silently rot. [INFERENCE — a format change and a trust-boundary change never share a plan.] -### 1.3 The sibling note — flagged, not resolved +### 1.3 The sibling note — named, landing beside this one The warrant capsule carries two arcs. This note is the register arc. The foundations arc — structure-instantiation as the bridge, the laws ledger, memberships first — -becomes **NEW NOTE — mathematical foundations and the laws ledger**, not yet written. +is **dn-mathematical-foundations** +(`docs/design-notes/dn-mathematical-foundations.md`), landing in this same PR. One shared boundary, flagged: the claim-ladder labels of §2.3 are *consumed* by the laws ledger (each law lands as a labeled claim with a falsifier); neither note should redefine the labels without the other. The float-epsilon caveat (float addition is @@ -346,7 +351,8 @@ Two guards on the rung agents will use most, because a plausible-but-wrong inlin its proof inline. Wired as template teaching comments, not new frontmatter. 2. **The deskcheck paper** — its Definitions-and-claims section (§2.4.3) is written in ladder labels; its Evaluation section discharges every Claim or says so honestly. -3. **The laws ledger** (sibling arc, when built) — each algebraic law lands as a +3. **The laws ledger** (dn-mathematical-foundations §2.2, `docs/LAWS.md`) — each + algebraic law lands as a labeled claim (typically Claim, or Proposition with its paired falsifier) with one falsifier per law; the label column is specified here so the sibling note consumes it, never redefines it. @@ -640,7 +646,8 @@ note's own lane. Closing the workflow lane still requires an approved dc naming manifest's RR rows — the board's phase function does not care which pipeline the dc was typed in. -**Explicitly NOT licensed:** the laws-ledger sweep (sibling arc); Lean; authoring the +**Explicitly NOT licensed:** the laws-ledger sweep (dn-mathematical-foundations +MF-1..MF-3); Lean beyond the sibling's L-ladder (its MF-4..MF-6); authoring the Question; retiring the HTML phone report; disposing of the dormant gate machinery; book chapter content beyond the registry extension; any parser change. @@ -678,7 +685,7 @@ not involved. | decision | default recorded | re-entry condition | |---|---|---| -| Lean / proof-assistant adoption | not adopted; "Theorem" stays effectively unreachable | a claim a property test cannot falsify (capsule park, unchanged) | +| Lean / proof-assistant adoption | L0 — ladder specified in dn-mathematical-foundations §2.4 (L1 = its MF-4 unit) | for L1: the laws ledger's first laws exist to state (issue #48) | | external venue / arXiv / DOI | none — internally reviewed technical reports only | the owner authors the Question and wants external referees | | brainstorm capsules adopting the register | chat stays vernacular; capture template gains only the Conjecture gloss (RR-1) | owner asks, after living with RR-1 | | HTML phone build report | kept for mid-track build waves; the dc PDF absorbs the track-closure role | two paper deskchecks delivered → owner reviews the overlap | diff --git a/docs/tracks/mathematical-foundations.md b/docs/tracks/mathematical-foundations.md new file mode 100644 index 0000000..47fe0a7 --- /dev/null +++ b/docs/tracks/mathematical-foundations.md @@ -0,0 +1,52 @@ +--- +type: track +slug: mathematical-foundations +title: Mathematical foundations — the laws ledger + the Lean ladder +status: active +warrant: null +audit_refs: [] +dod: + - MF-1 laws ledger seeded (docs/LAWS.md) — one row per law naming the TRUE structure, ladder-labeled (labels from dn-research-register §2.3); memberships lands multiset, never Boolean algebra + - MF-2 laplacian/spectral falsifier batch green or counterexamples filed (direct PSD, nullity = components, isolated-node convention) + the minimal ledger checker (anchors + test ids) + - MF-3 cut/conductance/curvature falsifier batch green or counterexamples filed (direct Φ(S) + both degenerate conventions; most_negative_edges emission rule) + - MF-4 formal/ L1 — sibling lake package builds; statements + Plausible attacks; sorry ratchet recorded; zero import coupling with core/ either direction + - MF-5 lean-action advisory CI green on a real PR with the Mathlib cache hitting + - MF-6 (entry-gated on MF-4) first L2 discharge batch — Theorem (machine-checked, formal/...) claimable for the discharged laws +backlog_deskcheck: null +links: + - docs/brainstorms/mathematical-foundations.md + - docs/design-notes/dn-mathematical-foundations.md + - docs/design-notes/dn-research-register.md +--- +# Track — Mathematical foundations (the laws ledger + the Lean ladder) + +The identity card for the mathematical-foundations track, minted alongside its +founding note (the scored-beliefs/erratum-relation precedent; ⚑ the owner renames or +rejects this coordinate at the merge). **Scope:** the mathematical substance of the +palace — which known structure each component is a model of +(structure-instantiation), the laws ledger (`docs/LAWS.md`: statement + arithmetic +domain, claimed structure, anchor, ladder label, falsifier, formal status per law), +the per-family falsifier batches, and the `formal/` Lean ladder (L1 statements → L2 +proofs; L3/L4 parked). Members are the artifacts declaring +`track: mathematical-foundations`. + +**Not in scope:** the research register (track: workflow — the §2.3 labels are +consumed here, never redefined); `core/` code changes (falsifier batches file +defects, never fix); Cheeger / Ollivier-Ricci formalization (L1 formalizes +definitions and stated laws only); the NOTATION.md refresh (its own surgical PR). + +## Relationship to other tracks + +`workflow` owns the claim ladder and the register this track writes in — labels flow +one way, from there to here. `erratum-relation`'s operator-algebra DoD rows are +candidate ledger rows once that lane's laws want indexing. `inner-outer-core`'s ring +discipline is the architecture-side analog of MEM-11 (the kernel-never-imports law); +`formal/` extends the same posture: a sibling like `eval/`, zero import coupling with +`core/` in either direction. + +**Definition of done:** the dod rows above — the ledger names true structures with +green paired falsifiers or filed counterexamples per family, `formal/` builds with +the sorry ratchet monotone down, the advisory CI job is green on a real PR, and the +first L2 discharge batch lands behind its entry gate. + +**Owed deskcheck:** none standing — nothing sealed on this track yet.