cert
plain-language theorem explainer
Packages three elementary facts about the domain cost into a single certificate for the scalar spectral index derivation: diagonal vanishing, nonnegativity on positive arguments, and positivity of the canonical threshold. Cosmologists citing the RS n_s prediction from the phi-ladder would use this bundle. The body is a pure structure assembly of three already-proved field lemmas.
Claim. There is a certificate asserting: (i) the domain cost of any nonzero real $r$ against itself vanishes, $\mathrm{domainCost}(r,r)=0$; (ii) for positive mass and energy parameters the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module derives the scalar spectral index $n_s$ from the Recognition Science phi-ladder and J-cost. Planck 2018 reports $n_s \approx 0.9649$; the RS inflation formula $n_s = 1 - 2/(N_e+1)$ with $N_e=44$ yields $0.9556$, consistent within roughly $3\sigma$.
The certificate structure collects the cost-side hypotheses needed for that derivation. Domain cost is the local cost functional on mass/energy pairs; it is required to vanish on the diagonal (self-comparison costs nothing) and to stay nonnegative for positive arguments. The canonical threshold is the positive cutoff against which spectral tilt is measured.
Upstream, nonnegativity of recognition cost is already forced by the J-cost minimum: any recognition event has $0 \le e.\mathrm{cost}$ because $J$ is nonnegative for positive state. The three field lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos specialize that fact to the cosmology domain.
proof idea
One-line structure construction. The three fields of nS3Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive mass and energy), and canonicalThreshold_pos (strict positivity of the threshold). No new algebra is performed; the definition only witnesses that those three facts inhabit the certificate type.
why it matters
Gives a single named inhabitant of the spectral-index certificate so downstream cosmology lemmas can assume cost hygiene without re-proving diagonal vanishing or threshold positivity. The module is marked structural (zero sorry, zero axiom) and sits in the Plan v7 pass that ties $n_s$ to the phi-ladder and J-cost. Framework landmarks in play are T5 J-uniqueness (the cost that underwrites nonnegativity) and the phi-ladder mass/yardstick structure used for inflationary tilt. No downstream users are recorded yet; the immediate sibling cert_inhabited is the natural consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.