CostFirstExistenceCert
plain-language theorem explainer
The CostFirstExistenceCert structure records three properties that together assert recognition existence holds exactly at the J-cost minimum x=1 for positive reals, with all other values carrying strictly positive cost that diverges as the argument approaches zero. Pre-Big-Bang selection researchers cite the certificate when grounding the claim that stable configurations arise solely from J-minimization. The structure is a direct record definition populated by three sibling lemmas.
Claim. A structure with three fields: (i) for all $x>0$, recognition existence of $x$ holds if and only if $x=1$, where recognition existence means $J(x)=0$; (ii) for all $x>0$ with $x≠1$, $J(x)>0$; (iii) no finite $C$ bounds $J(ε)$ from above for all $ε>0$.
background
The module formalizes the cost-first selection principle: a positive real exists in the recognition sense precisely when its J-cost vanishes. RSExists(x) is defined locally as Jcost x = 0 and shown equivalent to x=1 by the sibling rsExists_iff_one. The upstream OntologyPredicates version augments this with the explicit conditions 0<x and defect x=0, while Jcost itself is imported as the Cost abbrev from Measurement.RSNative.Core.
proof idea
The declaration is a structure definition. Its single downstream use site costFirstExistenceCert populates the three fields directly from the sibling lemmas rsExists_iff_one, non_existence_has_positive_cost, and divergence_at_zero_direction.
why it matters
The certificate supplies the structural backbone for the cost-first existence principle that selects stable configurations by J-minimization. It is consumed by costFirstExistenceCert and thereby supports the pre-Big-Bang claim that laws emerge from the unique J-minimizer at x=1. This step precedes the forcing chain that extracts phi, the eight-tick octave, and D=3 from the same minimum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.