nS3Cert
plain-language theorem explainer
Certificate structure bundling three algebraic properties of the domain cost and the canonical threshold used in the scalar spectral-index derivation from J-cost. Cosmologists tracing the RS inflation ladder (n_s ≈ 0.96) cite it when discharging the structural side conditions. Pure structure definition: no proof body, only field signatures.
Claim. A scalar-spectral-index certificate is a triple of facts: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for every $r\neq 0$; (ii) the domain cost is nonnegative on positive arguments, $m>0$, $e>0$ $\Rightarrow$ $\mathrm{cost}(m,e)\ge 0$; (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 gives $n_s=1-2/(N_e+1)=1-2/45=0.9556$, within about $3\sigma$. Status is structural: zero sorry, zero axiom.
Domain cost is the two-argument cost used on the inflationary field/energy plane; the certificate demands it vanish when the two arguments coincide (identity recognition) and stay nonnegative off-diagonal. Canonical threshold is the positive cutoff that separates the slow-roll window from the exit regime.
Upstream, nonnegativity of recognition cost is already forced: every recognition event has cost $\ge 0$ because $J$-cost is nonnegative on positive states (ObserverForcing.cost_nonneg). The certificate lifts that global fact to the concrete domain-cost map used here.
proof idea
No proof: this is a structure declaration. The three fields are Prop-valued hypotheses that any inhabiting instance must supply. Downstream, cert fills them by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then packages that instance as Nonempty nS3Cert.
why it matters
Gives a single named bundle for the side conditions of the spectral-index-from-J-cost argument, so later lemmas can assume one certificate rather than three loose hypotheses. Parent uses are the concrete witness cert and the inhabitation theorem cert_inhabited in the same module.
In the broader RS chain this sits under the cosmology layer that converts the forced J-cost (T5) and the phi self-similarity fixed point (T6) into an inflationary $n_s$. The module claims consistency with Planck within $3\sigma$; the certificate is the structural gate that makes that claim machine-checkable rather than narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.