cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single certificate that the RS Euler-number structure is inhabited: diagonal cost vanishes, cost is nonnegative on the positive quadrant, and the canonical threshold is positive. Anyone citing the structural Euler-number package in Foundation will point here. The body is a pure structure constructor wiring three sibling lemmas.
Claim. There exists a certificate for the RS Euler-number structure: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$ the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
The module treats Euler's number $e$ as a structural object in Recognition Science, comparing classical $e\approx 2.718$ with phi-ladder candidates such as $\varphi^\varphi$ and $\varphi^{D-\varphi^{-1}}$. Status is structural (zero sorry, zero axiom).
The structure being certified demands three properties of a domain cost on pairs of reals: vanishing on the diagonal away from zero, nonnegativity when both arguments are positive, and positivity of a fixed canonical threshold. Domain cost is the local cost functional used in this Foundation layer; the nonnegativity pattern matches the global recognition-event cost law (J-cost is nonnegative for positive state).
Upstream, ObserverForcing already records that every recognition event has nonnegative cost via Jcost_nonneg. The present certificate is the analogous packaging for the Euler-number domain cost and threshold.
proof idea
One-line structure instance. The three fields of EulerNumberERS are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No further tactic work; the definition is pure wiring of already-proved facts into the structure.
why it matters
Gives a single named witness that the RS Euler-number interface is inhabited, so downstream Foundation material can assume the three cost/threshold axioms without re-proving them. The module frames this as a structural theorem tying classical $e$ to phi-ladder geometry (T6 forces $\varphi$ as the self-similar fixed point; T8 forces $D=3$). No downstream users are recorded yet; the natural consumer is any theorem that needs a packaged Euler-number certificate rather than the three lemmas separately. Closes the local "is the structure nonempty?" obligation for this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.