PhiSqIdentCert
plain-language theorem explainer
Certificate structure bundling three analytic facts used by the phi-square identity module: domain cost vanishes on the diagonal, is nonnegative off it for positive arguments, and the canonical threshold is positive. Downstream code cites the inhabited instance rather than rebuilding the bundle. Pure definitional packaging of field obligations; no proof body.
Claim. A $\phi$-square identity certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (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 records the algebraic identity $\phi^2 = \phi + 1$, the defining fixed-point relation for the golden ratio in Recognition Science, and notes that the Fibonacci recurrence is the corresponding recognition recursion. Status is structural (zero sorry, zero axiom).
Domain cost is the real-valued cost assigned to a pair of positive scale parameters (measure and event, or analogous coordinates). The diagonal condition says matched scales carry zero cost. Nonnegativity is the local form of the global recognition-cost law. The canonical threshold is the positive cutoff used to separate identity-scale events from costly ones.
Upstream, ObserverForcing already proves that every recognition event has nonnegative cost via the J-cost minimum at $x=1$. The present structure re-packages the domain-level analogues of that fact together with diagonal vanishing and threshold positivity.
proof idea
No proof: this is a structure declaration. The three fields are Prop-valued obligations (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Inhabitation is supplied later by the definitional value cert, which plugs in the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named bundle for the analytic side-conditions that sit beside the algebraic identity $\phi^2=\phi+1$. Downstream, cert fills the three fields, and cert_inhabited records Nonempty of the certificate type, so later modules can assume the bundle without re-proving each clause.
In the forcing chain this supports T6: $\phi$ as the self-similar fixed point. The Fibonacci consequence stated in the module doc (recognition recursion identity) rides on the same algebraic relation. The certificate does not itself prove $\phi^2=\phi+1$; it packages the cost-theoretic hygiene that the identity module exposes to consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.