EulerNumberERS
plain-language theorem explainer
Interface record for the RS Euler-number construction: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Downstream certificates inhabit it by plugging in the three sibling lemmas. Pure structure definition with no proof body.
Claim. A certificate is a triple of properties: $\mathrm{domainCost}(r,r)=0$ for every $r\neq 0$; $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; and the canonical threshold satisfies $\mathrm{canonicalThreshold}>0$.
background
The module treats Euler's number $e$ as a structural constant in Recognition Science, related (at the level of the module sketch) to powers of the golden ratio $\varphi$ rather than to a transcendental series definition. Status is structural: zero sorry, zero axiom.
domainCost is the local cost functional on pairs of real arguments (measure-like and expectation-like inputs). The first field demands that cost vanish when the two arguments coincide and are nonzero. The second field is the domain-level nonnegativity statement, parallel to the upstream recognition-event fact that "the cost of any recognition event is non-negative" (cost_nonneg via Jcost_nonneg).
canonicalThreshold is the positive cutoff used by the Euler-number certificate; its positivity is the third field. Together the three fields form the Prop-bundle that later cert fills.
proof idea
No proof: this is a structure declaration. Each field is a named hypothesis (a Prop). Inhabitation is deferred to the sibling cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three slots, and to cert_inhabited, which wraps that assignment as Nonempty.
why it matters
Gives a single named type for the three structural obligations of the RS Euler-number package, so downstream code can depend on one interface rather than three free-floating lemmas. Immediate consumers are cert (the concrete witness) and cert_inhabited (nonemptiness). Fits the Foundation layer's pattern of packaging cost axioms before linking constants such as $e$ to the $\varphi$-ladder and the forcing chain (T5 J-uniqueness, T6 $\varphi$ fixed point). Does not itself derive the numerical value of $e$ or close any open analytic identification with $\varphi^{\varphi}$ or $\varphi^{D-\varphi^{-1}}$; it only freezes the cost/threshold interface those arguments will use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.