cert
plain-language theorem explainer
Packages three elementary properties of the RS domain cost into a single EFT2 certificate: vanishing on the diagonal, nonnegativity for positive mass and energy, and positivity of the canonical threshold. Anyone citing the structural EFT power-counting claim from J-cost will point here. The definition is a pure structure assembly of three already-proved sibling lemmas.
Claim. There is an EFT2 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 develops EFT power counting from the Recognition Science J-cost. In ordinary EFT, higher-dimension operators are suppressed by $(E/\Lambda)^n$. Under RS with spatial dimension $D=3$ (forcing step T8), the leading correction is $J(\varphi),(E/\Lambda)^3$. At the self-similar point $E=\varphi\Lambda$ this evaluates to $J(\varphi),\varphi^3=1/2$, a structural identity rather than a fit.
The domain cost is the local cost functional used to compare mass and energy scales in that counting. The certificate structure records the three algebraic facts needed before any power-counting inequality can be stated: the cost vanishes when the two arguments coincide, stays nonnegative in the physical quadrant, and the reference threshold (tied to the $\varphi$-ladder) is positive.
Upstream, nonnegativity of recognition cost is already known from ObserverForcing: every recognition event has cost $\ge 0$ because $J$ itself is nonnegative on positive reals.
proof idea
One-line structure instance. The three fields of EFT2Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional tactic work or algebraic reduction occurs at this declaration.
why it matters
This is the packaged witness that the domain-cost side of the EFT-from-J-cost story is algebraically clean (module status: structural theorem, zero sorry, zero axiom). It sits under the Plan v7 session-3 claim that the leading RS correction is $J(\varphi)(E/\Lambda)^3$ and equals $1/2$ at $E=\varphi\Lambda$.
Framework landmarks: T5 forces the unique J-cost $J(x)=(x+x^{-1})/2-1$; T6 forces $\varphi$ as the self-similar fixed point; T8 forces $D=3$, which supplies the cubic power. The certificate does not itself derive the cubic law; it only certifies the cost primitives that any such derivation must use.
No downstream consumers are recorded yet; the natural parent is any theorem that states the $(E/\Lambda)^3$ suppression or the half-unit correction at the $\varphi$ threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.