PiPhiRelRS
plain-language theorem explainer
A certificate structure packaging three properties required for the RS pi–phi relation: domain cost vanishes on the diagonal, domain cost is nonnegative for positive arguments, and the canonical threshold is positive. Downstream inhabitation (`cert`) and `Nonempty` proofs cite it. Pure structure definition with no proof body.
Claim. A pi–phi relation certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals 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 develops the Recognition Science link between $\pi$ and the golden ratio $\varphi$, with the working approximation $\pi \sim 4/\sqrt{\varphi}$ (about 0.15% relative error). Status is structural: zero sorry, zero axioms.
Domain cost is the local cost functional on pairs of positive reals (measure vs expectation style arguments) used to score recognition mismatch; it is expected to sit at the J-cost minimum on the diagonal. The canonical threshold is the positive cutoff against which that cost is compared when certifying the pi–phi relation.
Upstream, nonnegativity of recognition-event cost is already available from ObserverForcing (cost_nonneg: cost of any recognition event is nonnegative, via Jcost_nonneg). The present structure lifts the same nonnegativity pattern to the domain-cost level and adds diagonal vanishing plus threshold positivity.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (cost_at_eq, cost_nonneg, threshold_pos). Inhabitation is deferred to the sibling definition cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named interface for the structural hypotheses of the RS pi–phi relation, so later results can depend on one bundle rather than three loose lemmas. Immediate consumers are cert (the concrete inhabitant) and cert_inhabited (Nonempty PiPhiRelRS).
In the broader forcing chain, $\varphi$ is the self-similar fixed point (T6). Relating $\pi$ to a pure power of $\varphi$ is a foundation-level consistency check between geometric constants and the RS cost calculus. The structure does not itself derive the numerical approximation; it only packages the cost and threshold axioms that any such derivation must respect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.