cert
plain-language theorem explainer
Packages three elementary properties of the golden-angle domain cost into a single certificate record: diagonal vanishing, nonnegativity for positive arguments, and positivity of the canonical threshold. Anyone citing the RS golden-angle structural theorem uses this inhabited certificate. The definition is a pure structure assembly from three sibling lemmas.
Claim. There is a 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 fixes the RS golden angle $\theta_G=2\pi,\varphi^{-2}=2\pi(1-1/\varphi)$, the irrational rotation angle that appears in phyllotaxis. Status is structural: zero sorry, zero axioms.
domainCost is the local cost functional on pairs of real scales used to force that angle; the certificate structure GoldenAngleCert packages the three properties needed before any forcing or uniqueness argument can run. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity at positive state.
Sibling facts supply the three fields: diagonal vanishing of domain cost, its nonnegativity on the positive quadrant, and positivity of the canonical threshold against which the angle is compared.
proof idea
One-line structure construction. The three fields of GoldenAngleCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional rewriting or case analysis occurs; the definition is pure assembly of already-proved facts into the certificate record.
why it matters
Gives an inhabited certificate that the golden-angle domain cost meets the minimal analytic hypotheses (zero on the diagonal, nonnegative off it, positive threshold). In the RS foundation this is the structural entry point for treating $\theta_G=2\pi\varphi^{-2}$ on the same footing as other forced geometric constants (phi from T6, eight-tick octave from T7, $D=3$ from T8). No downstream consumers are wired yet in the graph; the companion cert_inhabited is the natural next step that witnesses nonemptiness of the certificate type. Closes the definitional half of the STRUCTURAL THEOREM claim in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.