cert_inhabited
plain-language theorem explainer
The golden-angle certificate bundle is inhabited: there exists a witness packing diagonal vanishing of domain cost, nonnegativity off the diagonal, and positivity of the canonical threshold. Anyone needing existence of that structural package (rather than the raw field lemmas) cites this. The proof is a one-line term that feeds the concrete certificate instance into Nonempty.
Claim. The type of golden-angle certificates is nonempty: there exists a record whose fields assert that domain cost vanishes on the diagonal for every nonzero real, is nonnegative for positive arguments, and that the canonical threshold is strictly positive.
background
The module fixes the RS golden angle $\theta_G=2\pi\phi^{-2}$ (equivalently $2\pi(1-1/\phi)$), the classical phyllotaxis angle, and packages its cost-side structural facts as a certificate.
domainCost is the local cost functional on pairs of reals used here; the certificate demands it vanish when both arguments equal a nonzero $r$, and stay nonnegative for positive mass/energy-style arguments. canonicalThreshold is the positive cutoff tied to that cost geometry.
GoldenAngleCert is the structure bundling those three propositions. Upstream, the module already builds a concrete instance cert satisfying the three fields; this theorem only records that the structure type is inhabited.
proof idea
Term-mode one-liner. The module already defines a concrete value cert : GoldenAngleCert. The proof is the anonymous constructor ⟨cert⟩, which is the standard Lean witness that Nonempty GoldenAngleCert holds. No tactics, no further lemmas.
why it matters
Gives a single inhabited certificate object for the golden-angle cost package inside Foundation, matching the module's STRUCTURAL THEOREM status (zero sorry, zero axiom). Downstream use list is currently empty, so this is an existence hook rather than a step inside a larger proved chain.
In the broader RS picture it sits with the golden ratio forced at T6 and the self-similar $\phi$-ladder geometry; $\phi^{-2}$ is exactly the fractional turn of the golden angle. It does not itself invoke J-uniqueness, RCL, or the eight-tick/D=3 forcing steps, but it keeps the phyllotaxis angle's cost certificate available as a typed unit for later foundation work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.