lean

8. Boundaries, countermodels, and nonclaims

The public theory is easiest to overstate at its seams. This chapter states the limits as part of the mathematics rather than as release trivia.

Exact nonclaims

1. No universal process semantics. GovernedFamily defines claims, evidence, books, and a total decision. It defines no process, transition relation, scheduler, or trace semantics. Other repository modules may define such objects, but the calculus root does not unify them. The crossing core explicitly defines no transition system (scope fence).

2. No global Admissible. The evidence-age licensing instance (Weathering) has a native judgment named Admissible. Paid reachability and BreakGlass keep different native substrates. The common predicate is derived Authority F c, always parameterized by a governed family and claim.

3. No runtime enforcement or conformance claim. A Lean checker definition does not prove that a deployed runtime called it, preserved its evidence, or mapped runtime objects correctly. The stable-root header lists the additional correspondence artifacts required (source).

4. No automatic composition of all kernels. The public crossing is binary and requires two GovernedFamily values with lossless refusal spines. It does not absorb the eight older admissibility kernels, all repository calculi, or arbitrary N-ary families. The separate kernels root disclaims a unified maximal calculus (source).

5. No universal subsumption theorem. The public comparison framework has seven indices and proof-bearing law shapes, but the concrete seven-entry ledger remains outside the public Lean surface. Ledger.covers is a theorem about any supplied ledger, not a public inhabitant containing those seven native comparisons.

Countermodels and hostile controls

Some negative evidence is public as a generic theorem; some is retained outside the public Lean surface:

Boundary	Public result	Retained non-public evidence
claim erasure	no_claim_erasing_check_is_faithful	Prop-squashing and full-claim controls
refusal encoding	no subsingleton exact domain	compiled constant-Unit collapse against the old contract
comparison exactness	collapsed/constant maps reject exact representation	instantiated seven-entry ledger and adapters
stored crossing	exact stored-pair coherence and non-shadowing	arbitrary-stored-pair hostile audit; legacy crossings
BreakGlass	origin-bound family, two separations, stored crossing	49-receipt hostile matrix, fixed-Atoms exploit, blocked predecessor packet

The table separates theorem meaning from publication status. Filenames alone do not determine whether an artifact is public Lean.

Narrow statements that preserve the evidence

• The exact codec preserves refusal packets. Accepted witness identity remains in the native decision.
• The bounded paid fixture proves admission-only reachability. Its paid-book custody is vacuous and its obligation book is empty.
• foldLocated carries input labels through the sanctioned construction. It does not authenticate raw labels or arbitrary relabeling.
• Exact judgment preserves a predicate in both directions. Exact representation additionally recovers source values.
• BreakGlass exceptional authority coexists with a retained denied ordinary verdict; it does not upgrade that verdict.
• The BreakGlass lifecycle is relative to supplied Atoms and a singleton audit trail. It proves no general transition universe, payment lifecycle, clock honesty, origin allocator, or cryptographic commitment.

Formal and repository status

Hostile audits, legacy exploits, concrete comparison adapters, and predecessor artifacts can support review without becoming imported Lean declarations. The claim register and readiness ledger record those publication boundaries.

The calculus is not uniformly axiom-free. The exact theorem footprints are enforced by check-calculus-footprint.sh. The BreakGlass footprint includes Quot.sound, Classical.choice, and its declared opaque public substrate; the exact split and ratification history are kept in the readiness ledger rather than repeated in the mathematical flow.

This site is open source. Improve this page.