FibLimitCert
plain-language theorem explainer
Certificate structure bundling three analytic hypotheses for the RS Fibonacci–φ limit: diagonal vanishing of domain cost, nonnegativity of domain cost on positives, and positivity of the canonical threshold. Cited by anyone assembling or inhabiting the Fibonacci–φ convergence certificate. Pure structure definition with no proof body; fields are filled by sibling lemmas.
Claim. A Fibonacci–$\phi$ limit certificate is a triple of properties: (i) domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for every $r\neq 0$; (ii) domain cost is nonnegative whenever both arguments are positive; (iii) the canonical threshold is strictly positive.
background
The module treats the classical limit $F_{n+1}/F_n\to\phi$ as self-similar fixed-point convergence in Recognition Science: $\phi$ is the attractor of the J-cost recursion (forcing step T6). Domain cost is the real-valued mismatch functional on pairs of positive reals that specializes the recognition J-cost; it is required to vanish when the two arguments agree and to stay nonnegative off the diagonal. The canonical threshold is a fixed positive real used as a quantitative cutoff in the convergence certificate.
Upstream, nonnegativity of recognition-event cost is already available from ObserverForcing (cost_nonneg: "The cost of any recognition event is non-negative"), which supplies the pattern this structure reuses at the domain-cost level.
proof idea
No proof body: this is a structure declaration. It packages three Prop-valued fields that later definitions discharge by pointing at sibling lemmas (domainCost_at_eq, domainCost_nonneg, canonicalThreshold_pos). Inhabitation is deferred to the downstream cert value and the Nonempty theorem built from it.
why it matters
Gives a single named type for the analytic side-conditions of the RS Fibonacci–φ limit, so the structural theorem (module status: 0 sorry, 0 axiom) can be stated as inhabitation of this certificate. Downstream, cert assembles a concrete inhabitant and cert_inhabited records Nonempty FibLimitCert. That closes the bookkeeping for the claim that $\phi=\lim F_{n+1}/F_n$ is the J-cost recursion attractor, tying the classical Fibonacci ratio limit to forcing landmark T6 (φ as self-similar fixed point) without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.