cert
plain-language theorem explainer
Packages three structural properties of the RS domain-cost model for the pi–phi relation into one certificate: diagonal vanishing, nonnegativity on positive arguments, and a positive canonical threshold. Anyone working the structural pi ≈ 4/√φ setup cites this inhabitant. The definition is a direct structure assembly from three already-proved component lemmas.
Claim. A certificate of the RS $\pi$–$\varphi$ relation: the domain cost vanishes on the diagonal ($\mathrm{cost}(r,r)=0$ for $r\neq 0$), is nonnegative for positive arguments, and the canonical threshold is strictly positive.
background
The module develops the Recognition Science structural link $\pi \sim 4/\sqrt{\varphi}$ (about $3.146$, within $0.15%$ of $\pi$). Status is a structural theorem with no sorry and no axioms.
The structure being inhabited asks for three facts about a real domain cost: it is zero when both arguments equal a nonzero $r$; it is nonnegative whenever both arguments are positive; and a fixed canonical threshold is positive. Those three fields are the entire interface.
Upstream, nonnegativity of recognition cost is already available from the observer-forcing layer (any recognition event has nonnegative $J$-cost). The present certificate specializes that idea to the domain-cost pair used for the $\pi$–$\varphi$ relation.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas that already prove diagonal vanishing of the domain cost, nonnegativity of the domain cost on positive reals, and positivity of the canonical threshold. No extra algebra is performed at this site.
why it matters
Gives a single named inhabitant of the RS $\pi$–$\varphi$ relation interface so downstream material can assume the three cost axioms without re-proving them. The module frames this as the structural theorem behind $\pi \sim 4/\sqrt{\varphi}$, tying the geometric constant $\pi$ to the golden-ratio fixed point forced in the T5–T6 segment of the forcing chain. No used-by edges are recorded yet; the natural consumer is any lemma that needs a packaged $\mathrm{PiPhiRelRS}$ hypothesis (including the sibling inhabitedness claim).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.