RevProb4Cert
plain-language theorem explainer
A certificate packing three analytic facts used by the RS sociology revolution-probability claim: domain cost vanishes on equal nonzero arguments, is nonnegative for positive mass and effort, and the canonical threshold is strictly positive. Downstream code builds a concrete inhabited instance from the matching lemmas. Pure structure definition with no proof body.
Claim. A certificate consists of three properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold (the $J(\varphi)^{-1}$ scale in the Tocqueville-style rate test) is strictly positive.
background
The module develops an RS reading of Tocqueville: revolution probability spikes when the rate of change crosses a fixed scale set by $J(\varphi)^{-1}$ times the improvement still needed. Here $J$ is the unique nonnegative cost fixed by the Recognition Composition Law, with $J(1)=0$ and $J(x)=(x+x^{-1})/2-1$.
Domain cost is the local cost functional on a pair of positive reals (mass-like and effort-like coordinates). The first field demands it vanish on the diagonal away from zero, matching the identity minimum of $J$. The second field is the sociology-level nonnegativity statement, parallel to the upstream recognition-event fact that every event cost is nonnegative via $J$-cost nonnegativity.
The canonical threshold is the positive constant against which improvement rates are compared; positivity is recorded as the third field so later probability statements never divide by a non-positive scale.
proof idea
No proof: this is a structure declaration. It only names three Prop-valued fields. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to the one-line Nonempty theorem that wraps that instance.
why it matters
Gives a single named bundle for the three side conditions the sociology layer needs before it can talk about revolution probability crossing the $J(\varphi)^{-1}$ threshold. Downstream, cert assembles a concrete value and cert_inhabited records that the type is nonempty, closing the structural theorem status claimed in the module header (zero sorry, zero axiom).
In the broader forcing picture this sits after T5 ($J$-uniqueness) and T6 ($\varphi$ as self-similar fixed point): the threshold scale is built from $J(\varphi)$, so the certificate is the sociology-facing interface to those foundation facts rather than a new derivation of them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.