Five minutesThe idea, in four stepsWhat the theory claims, in the order a reader needs it: ontology, geometry, dynamics, observable. No prerequisites.
The mathematicsThe boundary as a mathematical objectWhy an autonomy boundary can be defined as a stable closure fiber of an attribution functor — and what that definition buys.
VerificationMachine-checked resultsThe Lean development body, the exact commands that reproduce it, and an honest ledger of what is not proved.
The theory in four steps
The programme is not an optimisation trick. It is a chain from a philosophical concept to a machine-checked theorem:
interventions may still occur; attribution is no longer penetrated
Layer I establishes the object · Layer II selects an equilibrium of it — separately
LAYER II MECHANICS
boundary sharpness κ
maintenance cost c0κ
uncertainty entropy καCF
A4, A5
V(κ)=c0κ+καCF
κ∗=αCF/c0
σ∗=1
The theory in one figure. Layer I establishes what the boundary is; Layer II is a separate variational theory that selects an equilibrium of it. The categorical apparatus is not machinery for deriving the two-term potential.
Step 1 · OntologyWhat is a boundary?An agent's autonomy boundary is defined as the stable closure fiber of an attribution functor on a category of causal interventions. This is a definition, not a measurement.
Definition
Step 2 · GeometryGive the boundary a coordinate: sharpness κThe object is projected onto a single scalar — how sharply the boundary discriminates. κ is what makes the object comparable across systems.
Definition
Step 3 · DynamicsTwo costs, one potentialMaintenance cost grows with sharpness; uncertainty entropy falls with it. Their sum is a potential whose minimum is the equilibrium sharpness.
Machine-Checked
Step 4 · ObservableA criterion you could measureAt the equilibrium the dimensionless ratio σ takes a definite value. Whether real agents exhibit it is an empirical question that has not been tested.
Empirical prediction
Read this before the mathematics. The formal layer is built and machine-checked. The empirical layer is empty: no real deployed agent system has been tested. Every page states which of the five labels applies — Definition, Assumption, Machine-Checked Theorem, Conjecture, Empirical Prediction.