Calibration as Closure: Laws as Compression Fixed Points under No-Free-Bits Paper 44 of the NEMS Suite
"Laws" are formalized as stable fixed points of an internal law-update operator driven by closure constraints; minimality is kept abstract (no MDL). Multiplicity of fixed points implies a selection problem. Under the SelectorStrength barrier schema (Paper 29), no total-effective decider exists for the uniform law-selector claim over an encoded family of law-update instances when anti-decider closure and a fixed-point premise hold on the code domain. Stratified law selection on restricted fragments remains possible. A minimal toy (two law types: minimal / other) witnesses multiplicity and the concept of minimal fixed points; the barrier applies to uniform selection across instances, not to the toy predicate. The development is mechanized in Lean 4 as the LawCalibration library in nems-lean, with zero sorry and no custom axioms. Trust boundary. Law-selection barriers apply to uniform deciders over encoded law-update families; fixed-point multiplicity and toy witnesses are not landscape theorems. Mechanization is nems-lean . See .
Authors
- Nova Spivack
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-09-13
- DOI
- https://doi.org/10.5281/zenodo.19429806
- Primary Topic
- Logic, programming, and type systems
- Type
- preprint