Nothing
plain-language theorem explainer
Nothing is formalized as the empty type to serve as the placeholder for non-existence in the meta-principle that nothing can recognize itself. Researchers deriving physics from recognition cost cite it when grounding the prohibition on self-recognition of the void at zero cost. The declaration is a direct abbreviation to Empty with no further reduction.
Claim. Let $E$ denote the empty type. Nothing is defined as $E$.
background
The Recognition module opens with T1, the meta-principle that nothing cannot recognize itself. Nothing is introduced as the type-theoretic stand-in for the void, corresponding in the cost framework to the limit $x → 0$ where the J-cost diverges to infinity. This abbreviation supplies the formal object used in downstream statements that no finite-cost configuration can approach or recognize the empty case.
proof idea
The declaration is a one-line abbreviation aliasing the empty type Empty.
why it matters
This definition supplies the formal content for the derived meta-principle MP in CostAxioms, where mp_from_cost proves that J(x) becomes arbitrarily large near zero and therefore nothing can be recognized at finite cost. It is referenced in unity_is_unique_existent, economic_inevitability, and scaffolds_remaining, closing the T1 step that feeds the forcing chain toward unique unity at x=1 and the subsequent derivation of phi and spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.