The predicate ledger of the corpus: the master ledger 00 and the ledger of every public paper, one predicate per row. A row is cited by its ledger and label, as 00:A1 or 35:P11, and each label opens the row in its own ledger. The accession key pNNNNN stays fixed while labels may move, and register.html#pNNNNN opens its row. The Filters choose a paper, a block and a status, and the search runs within the choice. Across all papers, a prediction or an explanation stated in more than one paper is listed once, at its first appearance, with its restatements linked.
Filters
| # | Predicate | Status | Sources |
|---|
Nothing matches that selection.
Status
- G
- ground — the single given that conditions the discourse
- T
- theorem — derived within the framework
- D
- definition — a naming or set-up move, no empirical content
- R
- realisation — what a physical term denotes in the substrate; forced (A8), each row stating the falsifier that kills it
- I
- import — a standard result or measured datum, used without reproof
- Ω
- Ω-hard — a value in no embedded reader's window, not closeable by a bounded observer; host-decided on any laboratory Carrier; never applied to a relation
- O
- open — genuinely unresolved
Sources
- The witnesses. Gold: the python check that decides the predicate, at its line in the script. Green: the predicate as one Lean declaration in the core, named by its accession key, proved with no axioms. Violet: the same on Mathlib. Red: a check that fails or a proof the gate rejects.
- section
- As on the ledger page: the statement in the paper's body that carries the predicate or, for a master predicate, the papers that state it.
- rests on
- The predicates it rests on or names, by label.