GoldenAngleCert
plain-language theorem explainer
A certificate packing three elementary properties of the RS domain cost and the golden-angle threshold: diagonal cost vanishes, cost is nonnegative on the positive quadrant, and the canonical threshold is strictly positive. Anyone wiring golden-angle geometry into the recognition cost calculus cites this bundle. It is a pure structure definition; inhabitance is discharged separately by the concrete cert.
Claim. A golden-angle certificate is a record of three facts: (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 fixes the RS golden angle $\theta_G = 2\pi,\varphi^{-2}$ (equivalently $2\pi(1-1/\varphi)$), the irrational rotation that appears in phyllotaxis. The surrounding development treats this angle as a structural consequence of the $\varphi$-ladder rather than an empirical fit.
Domain cost is the local cost functional on pairs of positive reals (measure versus expectation, or two radial scales). Its diagonal vanishing and nonnegativity mirror the global J-cost facts: $J(1)=0$ and $J\ge 0$, the latter already recorded upstream as "the cost of any recognition event is non-negative" via Cost.Jcost_nonneg. The canonical threshold is the positive cutoff used to separate trivial from nontrivial angular recognition events.
The certificate is the minimal Prop-bundle those three facts must satisfy before golden-angle constructions may be invoked.
proof idea
No proof body: this is a structure declaration. The three fields are pure propositions. Downstream, the noncomputable definition cert fills them by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Inhabitance is then the one-line ⟨cert⟩.
why it matters
Gives a single named interface for the cost and threshold hypotheses that golden-angle arguments need, so later lemmas do not restate three separate assumptions. Downstream cert and cert_inhabited discharge the interface inside the same module, marking the golden-angle development as a structural theorem (zero sorry, zero axiom) in the module status line.
In the broader RS chain the golden angle is the angular counterpart of the self-similar fixed point $\varphi$ forced at T6; packaging its cost hypotheses keeps the geometric layer aligned with the J-cost calculus (T5) and the eight-tick / three-dimensional forcing (T7–T8) without smuggling extra axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.