NecessityGate
plain-language theorem explainer
NecessityGate supplies the uniform record type that collects the six choke-point constraints any alternative framework must violate under the cost-as-foundation view. Researchers comparing zero-parameter theories to Recognition Science cite the structure when checking against cost uniqueness, discreteness, ledger symmetry, phi forcing, or dimension forcing. The declaration is a direct three-field record definition with no lemmas or computation.
Claim. A necessity gate is a record consisting of a string identifier for the constraint, a boolean marking whether the constraint has been proven, and a string describing the physical consequence of its violation.
background
The module formalizes the inevitability structure of Recognition Science by relocating the bottleneck from a tautology about Empty to the physical claim that selection occurs by minimizing a unique cost. Alternatives therefore fall into three buckets: choices about the cost functional J itself, choices about what existence means, and choices about the admissible class of frameworks. Under analyticity, symmetry, convexity and normalization, J is forced to the unique form J(x) = ½(x + x⁻¹) - 1 (T5).
proof idea
Direct structure definition introducing the three-field record type. No tactics or lemmas are applied; the type is populated by sibling definitions such as gate_cost_uniqueness and gate_dimension.
why it matters
The structure supplies the common type for all_gates, which enumerates the six necessities that realize the inevitability theorem. It is instantiated by gate_cost_uniqueness (T5), gate_discreteness, gate_ledger, gate_phi, and gate_dimension (D = 3). The construction therefore connects the forcing chain T5–T8 to the claim that any zero-parameter framework must reduce to RS or break one of these gates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.