cert
plain-language theorem explainer
Packages three elementary facts about the gap-45 domain cost into a single certificate record: diagonal vanishing, non-negativity on positive pairs, and positivity of the canonical threshold. Anyone citing the Gap45 exact structural theorem uses this as the inhabited witness. The body is a pure structure assembly of three sibling lemmas.
Claim. There is a certificate asserting: (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 is strictly positive.
background
The module proves the exact gap-45 identity $45 = D^2(D+2) = 9\cdot 5$ as a structural theorem forced by $D=3$, with zero sorry and zero axioms. The same integer appears as the classical $45^\circ$ range angle, $\pi/4$ key angle, and related numerology listed in the module header.
domainCost is the local cost functional on pairs of positive reals used in this gap argument. The certificate structure Gap45ExactV2Cert packages the three properties needed downstream: the cost vanishes on the diagonal away from zero, stays nonnegative for positive arguments, and the associated canonical threshold is positive. Non-negativity of recognition costs is the same qualitative fact as cost_nonneg in ObserverForcing ("The cost of any recognition event is non-negative"), specialized here to the domain-cost presentation.
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No further rewriting or case analysis occurs.
why it matters
Supplies the inhabited certificate that the Gap45 exact v2 development needs in order to treat gap-45 as a closed structural fact forced by $D=3$ (forcing-chain landmark T8). The module status line marks the whole development as a structural theorem with no axioms. No downstream consumers are recorded yet in the graph; the immediate sibling cert_inhabited is the natural next step that turns this definition into a non-emptiness witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.