cert
plain-language theorem explainer
Packages a certificate that the RS domain cost vanishes on equal nonzero arguments, stays nonnegative for positive mass and energy, and that the canonical threshold is strictly positive. Anyone wiring Euler–phi structural claims into the cost layer would cite this bundle. The definition is a three-field structure instance filled by named sibling lemmas.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module treats structural links between Euler's number $e$ and the golden ratio $\varphi$ inside Recognition Science, with status marked as a structural theorem (no sorry, no axioms). The local cost object is a two-argument domain cost on real mass and energy scales, meant as a J-cost style defect between those scales.
The certificate structure EulerPhiCert packages three elementary positivity and diagonal-vanishing facts about that domain cost plus a positive canonical threshold. Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: the cost of any recognition event is nonnegative, via nonnegativity of $J$.
Sibling facts supply the three fields: diagonal vanishing of domain cost, its nonnegativity on the positive quadrant, and positivity of the canonical threshold.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas for diagonal vanishing of domain cost, nonnegativity of domain cost on positive arguments, and positivity of the canonical threshold. No extra rewriting or case analysis.
why it matters
Gives a single named witness that the Euler–phi domain-cost layer satisfies the minimal cost axioms (zero on the diagonal, nonnegative off it, positive threshold). Downstream use is not yet wired in this graph (no used_by edges), so the declaration is a packaging point rather than a forcing-chain step.
In the broader RS picture it sits with the J-cost infrastructure (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$) and the $\varphi$-ladder constants, preparing structural comparisons of $e$ and $\varphi$ without claiming a closed transcendental identity. Module notes stress that $e$ and $\varphi$ are transcendentally independent while still admitting structural RS expressions; this certificate only underwrites the cost side of that discussion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.