The epistemic ledger

Every claim, its tag, and where its evidence lives

This page is the site's index of what is known and how it is known. It is not a disclaimer — the disclaimers are on the Scope page. This is an inventory: for each statement the theory makes, which of five tags it carries, and where a reader can go to check it.

The rule that generates the tags

The programme holds itself to one discipline, and it is the reason this site is organised the way it is:

A claim may enter only in one of two legal forms — (1) a declaration that compiles in Lean with zero

sorry

, or (2) a faithful report of a cited source. Everything else is an interpretation, must carry its tag, and may not appear in a theorem position.

Theorem and interpretation are kept strictly apart — the paper calls this the wall of caution. "Theorem" means proved, classically or in Lean, and nothing else.

Tag	Means	How a reader checks it
Definition	A stipulation. Nothing to prove; it fixes vocabulary.	Read it; check it is used consistently.
Assumption	A premise the theory does not derive.	Ask whether it holds of the system you care about.
Machine-Checked	A theorem with a machine-checked proof.	Run the reproduction command.
Conjecture	Stated, not proved. May be false.	Look for a counterexample.
Empirical prediction	A claim about the world, untested.	Run the experiment; it is designed to be able to fail.

The ledger

Definitions

Statement	Where
$Caus$ — the category of causal interventions	Object
$A : Caus^{op} \to Δ^{2}$ — the attribution functor	Object
$B = StableClosureFiber (A)$ — the boundary	Object
$\partial = (Fix (c), b)$ — the two-part decomposition	Object
$V (κ) = c_{0} κ + α C_{F} / κ$ — the potential	Mechanics
$σ = σ_{0} κ^{2}$ — the tension	Observable

Assumptions

Statement	Status of the assumption
A1–A3 — compatibility of the attribution functor with intervention	Chosen. They define the object; nothing forces them.
A4–A5 — the entropic and maintenance terms enter the potential	Chosen as the value-layer setting.
A6 — the calibration identity (equivalent to the logistic form of the kernel)	The single substantive assumption. It is the foundation of this work, not a result of it, and is permanently confined to the assumption environment. Assumption
A7 — maintenance cost is additive over disjoint subsystems and continuous in sharpness	Natural, statable, and falsifiable. It is what forces linearity. Assumption
The variable identification — $κ \leftrightarrow$ stiffness, and its companions	Not derived. This is the hypothesis under test. Mapping hypothesis

Machine-checked theorems

Statement	Where
The intervention category is free, with its universal property	Categorical layer
Cohesion is a closure operator; the boundary is its fixed-point set	Object
The defect is a decidable obstruction class	Categorical layer
The entropic term: $H (κ) = C_{F} / κ$ , antitone in $κ$	Mechanics
Without A7 the maintenance term is free (two admissible models exist)	Mechanics
Under A7 the maintenance term is linear: $M (κ) = c_{0} κ$	Mechanics
Non-categoricity: the potential is determined only up to $c_{0}$	Mechanics
Unique minimum $κ^{} = α C_{F} / c_{0}$ , with $V^{} = 2 c_{0} κ^{*}$	Observable
$σ^{} = α C_{F} / C_{0}$ , and $σ^{} = 1 ⟺ π^{2} α = 3 C_{0}$	Observable
The critical locus branches; the projection is a branched cover	Observable
The algebraic core of the conservation: force is minus the gradient; the energy bracket vanishes	Observable
The attractor has a unique fixed point and an exact geometric rate	Observable
The universality split: G4 holds at the state layer, fails at the kernel layer	Observable

Conjectures and open items

Item	Why it is open
The origin of the kernel	Not derived; the family is classified, not explained.
Why the two symmetries hold	Geometric contraction is derived from them; their own ground is not given.
The experimental decision procedure for "settled"	Stated as a protocol; not implemented.
The step-to-second mapping	No derivation.
Cross-domain docking additivity	No definition, no theorem, no test. Should not be treated as a premise. Conjecture

Empirical predictions

Item	Status
P1 — $σ$ clusters near $1$ across a controller population	Not run
P2 — the balance-loop frequency is $ω = 2$	Not run
P3 — stiffness and estimator entropy covary as $σ \propto H^{- 2}$	Not run
The three anchors as falsifiable correspondences	Mapping hypotheses

Explicitly not claimed

Not claimed
Any commitment to qualia, phenomenal consciousness, or first-person experience.
Any use of, or commitment to, the free-energy principle.
That any real system has been tested.
That the formal class captures autonomy in general. Whether it does is the empirical question.

How to use this page. If a statement you are reading elsewhere does not appear here, it is not part of the theory's ledger — treat it as commentary. If it appears with a tag, that tag is the theory's own claim about its own strength. Where the tag says Machine-Checked, the reproduction command is the evidence; where it says Conjecture or Empirical, nothing has been proved.