cert
plain-language theorem explainer
Packages three elementary properties of the domain cost into a single certificate for the sigma8-from-J-cost argument: the cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cosmologists citing the RS account of the CMB/weak-lensing sigma8 split would reach for this witness. The body is a pure structure assembly from three already-proved sibling lemmas.
Claim. There exists a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the observational sigma8 tension: CMB prefers $\sigma_8 \approx 0.83$ while weak lensing prefers $\approx 0.77$. Recognition Science reads the ratio $0.77/0.83 \approx 0.928$ against $1 - J(\varphi) \approx 0.882$, predicting a roughly twelve-percent suppression from BIT structure formation, in the observed direction.
The domain cost is the local cost functional on model/environment pairs used in that comparison. The certificate structure demands three structural facts about it: vanishing when model equals environment (away from zero), nonnegativity on the positive orthant, and positivity of a fixed canonical threshold. Upstream, nonnegativity of recognition cost is already known from the observer-forcing layer via nonnegativity of $J$.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas that the domain cost equals zero on the diagonal, that the domain cost is nonnegative for positive arguments, and that the canonical threshold is positive. No new arithmetic is performed.
why it matters
Gives a single named witness that the cost side of the sigma8-from-J-cost story is structurally sound (zero sorry, zero axiom in the module). Downstream consumers can assume the certificate rather than re-prove diagonal vanishing, nonnegativity, and threshold positivity. It sits under the broader RS claim that the CMB/WL split tracks $1-J(\varphi)$ from the T5 J-uniqueness and T6 golden-ratio fixed point, rather than new dark-sector parameters. No used-by edges are recorded yet; the certificate is the export surface for later numerical or observational hooks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.