Boundary / Axiom

Public site 1.0.1 · machine-checked core

The boundary
is the report.

A log can be stale. A report can be decoration. The question is whether a boundary and its report are two objects — or one.

Read the programme The formal core →

The claim

On the class of Moore report families, a boundary closure operator and the system's report family determine each other. The report family is exactly the fixed-point family of the operator. Outside that class, the identity fails — and there is a machine-checked counterexample.

The result is conditional and narrow. It does not say that every autonomous system has a Moore family, that the attribution layer has been bridged to the closure layer, or that a deployed agent cannot bypass the gate. Those are separate claims, and they are not made here.

Evidence, without inflation

467 theorems and lemmas.
90 definitions. Zero sorry.

56Lean files
467Theorems / lemmas
90Definitions
0Sorry / custom axioms

This is the full verified corpus. The report-identity core is a six-module / 45-theorem subset under report-core/; the A-module contributes 33 declarations. The numbers answer different questions and are not interchangeable.

What is proved

  • cR is a closure operator for any report family.
  • Moore families determine their closure uniquely.
  • Report = closed sets is a joint fixed point, not a metaphor.
  • Representation: every Moore family is a closure's fixed family.
  • The condition cannot be dropped: a non-Moore counterexample.
  • A finite gate with R1–R7 and atomic commit, 14/14 tests.

What is not claimed

  • Not universal. Conditional on the Moore structure.
  • Not the attribution bridge. A → closure is still open.
  • Not a unique level. The parameter w is not fixed by V.
  • Not A7 from category. The potential is a model-class result.
  • Not production. The gate is a finite-state reference.
  • Not a theory of consciousness. Functional and architectural only.

Artifacts

ProgrammeWhy the claim matters; what the programme refuses to claim. Technical editionDefinitions, results, negative control, scope. Evidence ledgerCounts by scope, hashes, build and gate records. Open bridgeThe attribution → closure gap, stated plainly. Report-identity coreSix modules; entry ReportIdentity. Gate referenceR1–R7 finite-state implementation.

The wager

Not a finished theory. A way to ask the question that keeps the answer honest.

If the relation can be made precise, it gives a way to talk about self-organisation without an inner observer — and a way to build systems whose reports are not decorative. The wager may fail. The formal condition may be too strong for an interesting system, or too weak to distinguish boundary cognition from ordinary control. The release is written so that those failures can be discovered.

Read what is proved See what is open →