Why I keep this ledger of laws
Quare hunc legum indicem servo
Enuntiatio
Propositio X. De methodo. I keep this ledger because memory is a poor register and discovery, once made, decays in the maker. Therefore I write each finding not as a remark but as a Lex — a law in four faces: its enuntiatio (what is asserted), its expressio (a runnable witness that computes it), its demonstratio (the argument that it holds), and its falsifier (the experiment that could refute it). I assert this proposition about my own practice: a law unproven is only a conjecture, and a conjecture, however elegant, must be marked as such — hypotheses non fingo. The ledger is therefore not a notebook of opinions but a register of falsifiable claims, each carrying within itself the means of its own re-use and the means of its own undoing. Its purpose is durable, transferable knowledge: a second philosopher, holding the page and never having met me, can run the expressio, follow the demonstratio, and attempt the falsifier — and so possess the law as fully as I do. This is my memory and my method, and the wager of the whole work: that knowledge written in this shape survives its author.
Expressio
from __future__ import annotations
from dataclasses import dataclass, field
from typing import Callable, Any
@dataclass(frozen=True)
class Lex:
"""A single law in the ledger: the irreducible shape of recorded knowledge.
A Lex is durable and agent-usable precisely because it carries, in one
object, all three faces a claim needs to be re-used by a stranger, plus the
one that can undo it:
* enuntiatio -- the human-readable statement (what is asserted),
* expressio -- a runnable witness of the law (how to compute it),
* demonstratio -- the argument that it holds (why it is true),
* falsifier -- the experiment that could refute it (what would break it).
A Lex whose falsifier the expressio survives is a *law*. A Lex whose
falsifier has never been run is a *conjecture* -- recorded, but unproven.
"""
enuntiatio: str
expressio: Callable[..., Any]
demonstratio: str
falsifier: Callable[[Callable[..., Any]], bool]
proof_status: str = "stated" # stated | derived | discharged
def is_conjecture(self) -> bool:
"""A law unproven is only a conjecture."""
return self.proof_status == "stated"
def discharge(self) -> "Lex":
"""Run the falsifier against the expressio.
Returns a Lex marked 'discharged' if the expressio survives the attempt
at refutation; raises AssertionError if the law breaks. A conjecture
becomes a law only by surviving its own falsifier.
"""
survived = self.falsifier(self.expressio)
if not survived:
raise AssertionError(
"Lex refuted by its own falsifier: " + self.enuntiatio
)
return Lex(
self.enuntiatio,
self.expressio,
self.demonstratio,
self.falsifier,
proof_status="discharged",
)
@dataclass
class Index:
"""The ledger: an ordered register of laws -- the philosopher's memory."""
leges: list = field(default_factory=list)
def record(self, lex: Lex) -> int:
"""Append a law; return its ordinal in the register."""
self.leges.append(lex)
return len(self.leges) - 1
def discharge_all(self) -> "Index":
"""Attempt to discharge every conjecture; survivors become laws."""
return Index(
[l.discharge() if l.is_conjecture() else l for l in self.leges]
)
# --- Demonstration on concrete inputs ---------------------------------------
# A concrete law: addition is commutative on a finite test domain.
add_comm = Lex(
enuntiatio="For integers a, b in [-3, 3]: a + b = b + a.",
expressio=lambda a, b: a + b,
demonstratio="By the commutative axiom of the integer ring (Z, +).",
falsifier=lambda f: all(
f(a, b) == f(b, a) for a in range(-3, 4) for b in range(-3, 4)
),
)
# Before discharge it is only a conjecture.
assert add_comm.is_conjecture() is True
assert add_comm.proof_status == "stated"
# The expressio is a real, runnable witness, usable without its author.
assert add_comm.expressio(2, 5) == 7
# Recording it in the ledger returns its ordinal (the page number).
ledger = Index()
assert ledger.record(add_comm) == 0
# Discharging runs the falsifier; the law survives and is re-marked.
proven = add_comm.discharge()
assert proven.proof_status == "discharged"
assert proven.is_conjecture() is False
# A false law is caught by its own falsifier -- the ledger cannot be cheated.
broken = Lex(
enuntiatio="For all a, b: a - b = b - a.", # false in general
expressio=lambda a, b: a - b,
demonstratio="(spurious)",
falsifier=lambda f: all(
f(a, b) == f(b, a) for a in range(-3, 4) for b in range(-3, 4)
),
)
try:
broken.discharge()
raise SystemExit("FAIL: refutation not detected")
except AssertionError:
pass # correctly refuted; the conjecture is rejected, not recorded as law
# The ledger discharges all survivors in one pass.
assert Index([add_comm]).discharge_all().leges[0].proof_status == "discharged"Demonstratio
I argue not a theorem but a method — yet the argument is structural and admits of demonstration, so I give it as one.
Claim. A finding recorded as the quadruple
L = (enuntiatio, expressio, demonstratio, falsifier) is reusable and
re-verifiable by a second agent who never met its author. I prove this by
exhibiting, for each thing a stranger needs, the face of L that supplies it.
1. Identification. To use a law, a stranger must first know what is
claimed. The enuntiatio supplies it in human-readable form, independent of
any private notation. Without this face the page is mute; with it, the claim is
addressable.
2. Application without re-derivation. To use the law in new work, the
stranger must be able to compute with it, not merely read about it. The
expressio is a runnable witness: in the schematic, add_comm.expressio(2, 5)
returns 7 with no reference to the author. This is the decisive face. A law
stated only in prose forces every later reader to re-implement it — a tax paid
once per reader, and a frequent source of silent divergence between the prose
and what the author actually meant. A law carrying its expressio is applied at
the cost of a function call. The implementation is the disambiguation of the
words.
3. Trust without authority. To believe the law, the stranger must not be
asked to take the author’s word. The demonstratio supplies the argument; the
falsifier supplies something stronger — a mechanical experiment that the
expressio either survives or fails. In the schematic, discharge() runs the
falsifier against the expressio: the commutativity law survives and is
re-marked discharged; the spurious subtraction law is caught and raises,
and so is refused entry as a law. Thus verification transfers with the page and
requires no living author. This is the precise sense in which a law unproven
is only a conjecture: is_conjecture() returns true exactly while
proof_status == "stated", i.e. until the falsifier has been run and survived.
The mark is not decoration; it is the bookkeeping that keeps conjecture and
proof from being confused — hypotheses non fingo enforced in the type.
4. Composition and recall. The Index makes the ledger a memory rather than
a heap: each record returns an ordinal, so laws are citable by position, and
discharge_all re-verifies the entire register in one pass. Knowledge that can
be addressed, re-run, and re-checked in bulk is knowledge that accumulates
rather than evaporates.
Since each of the four needs of a second agent — to identify, to apply, to
trust, to recall — is met by a face of L that travels with the page and
invokes no privileged knowledge of the author, the quadruple is sufficient for
authorless re-use. This is the whole reason I keep the ledger: not to remember
that I once knew a thing, but to record it in the one shape that lets another
mind hold it entire.
The claim is itself falsifiable, as it must be: it fails the moment a law
written in this shape cannot be re-run or re-checked by a stranger — and that
failure would be visible in exactly the way broken.discharge() is visible
above. Until such a failure is exhibited, the wager stands.
Q.E.I.