cert
plain-language theorem explainer
Packages the three structural hypotheses of the primordial GW certificate: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Cosmologists citing the RS prediction r = 2/(45 φ²) ≈ 0.017 use this as the inhabited witness. Proof is a three-field structure instance wiring existing lemmas.
Claim. There exists a certificate asserting: (i) for all $r \neq 0$, the domain cost at $(r,r)$ is zero; (ii) for all $m,e > 0$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module derives the primordial tensor-to-scalar ratio from the Recognition Science J-cost. Status is structural (zero sorry, zero axiom). The RS value is $r = 2/(45\varphi^2) \approx 0.0170$, inside the Planck+BICEP bound $r < 0.036$.
PrimGW3Cert is the structure that packages three elementary cost facts needed before any amplitude comparison: diagonal vanishing of the domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold. Domain cost is the local cost functional on mode pairs; the canonical threshold is the positive cutoff against which the GW amplitude is compared.
Upstream, nonnegativity of recognition cost is already forced: any recognition event has cost $\ge 0$ because $J$ is nonnegative on positive reals (cost_nonneg from ObserverForcing, via Jcost_nonneg).
proof idea
One-line structure instance. The three fields of PrimGW3Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No further tactic work; the definition is pure wiring.
why it matters
This is the inhabited certificate object for the primordial-GW-from-J-cost structural theorem (Plan v7, 116th pass). It does not itself compute $r$; it records that the cost side of the argument is well-posed: zero on matched modes, nonnegative elsewhere, with a positive threshold. Downstream consumers (none yet linked in the graph) would cite cert or cert_inhabited when discharging the certificate hypothesis of any amplitude bound. Framework landmark: J-cost nonnegativity (T5 lineage) underwrites the second field; the numerical claim $r \approx 0.017$ sits inside the observational window without further axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.