cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single FibLimitCert witness for the Fibonacci ratio limit. Anyone citing the RS claim that F_{n+1}/F_n converges to the self-similar fixed point φ will use this certificate as the structural handle. The definition is a pure structure assembly: it wires three already-proved sibling lemmas into the certificate fields.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for every nonzero real $r$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive. Together these form the FibLimitCert witness used by the Fibonacci–$\varphi$ limit development.
background
The module treats the classical limit $F_{n+1}/F_n\to\varphi$ as the attractor of the J-cost recursion in Recognition Science. Here $\varphi$ is the unique self-similar fixed point forced by the T5/T6 chain (J-uniqueness and the fixed-point equation), and the Fibonacci ratios are the discrete orbit that converges to it.
Domain cost is the local cost functional on pairs of positive reals that vanishes exactly on the diagonal and stays nonnegative off it. The canonical threshold is a strictly positive cutoff used to separate the attractor basin from transient ratios. FibLimitCert is the structure that bundles exactly those three properties: diagonal vanishing, nonnegativity, and positive threshold.
Upstream, nonnegativity of recognition cost is already available from ObserverForcing (cost_nonneg: the cost of any recognition event is non-negative), which underwrites the domain-cost nonnegativity field.
proof idea
One-line structure construction. The three fields of FibLimitCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional reasoning is performed at this site; the definition is pure packaging of already-established facts.
why it matters
In the RS forcing chain, T6 forces $\varphi$ as the self-similar fixed point of the J-cost recursion. This certificate is the local structural witness that the domain-cost geometry needed for the Fibonacci-ratio attractor is in place: cost vanishes on equal ratios, never goes negative, and a positive threshold exists. The module advertises the whole development as a structural theorem (0 sorry, 0 axiom).
No downstream consumers are recorded yet (used_by is empty), so the certificate currently stands as the inhabited handle for later limit or convergence arguments in the same module (e.g. via cert_inhabited). It does not itself prove $F_{n+1}/F_n\to\varphi$; it only certifies the cost-side hypotheses those arguments will need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.