cert
plain-language theorem explainer
Packages three domain-cost facts (vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive) into one Tribonacci certificate. Cited by anyone needing a witness that the D=3 recognition cost setup is well-posed. Pure structure instance: wires three already-proved sibling lemmas, no new algebra.
Claim. There is a certificate asserting: (i) for every nonzero $r\in\mathbb{R}$, the domain cost of $(r,r)$ is zero; (ii) for all positive measured and expected values $m,e>0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats the Tribonacci constant $T\approx 1.839$ (root of $T^3=T^2+T+1$) as a structural object at spatial dimension $D=3$: the recognition chain then has three prior terms. The note stresses that $T$ is not simply a power of $\varphi$ (e.g. not $\varphi^2$ or $\varphi^{3/2}$); the link is structural rather than a direct ladder identity.
TribonacciCert is the bundle of three cost axioms needed for that story: diagonal vanishing of the domain cost, nonnegativity for positive arguments, and positivity of a canonical threshold. Domain cost is the local cost functional on measured/expected pairs; the threshold is the positive cutoff used to gate recognition events.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via $J$-cost nonnegativity at positive state. The three field proofs (domainCost_at_eq, domainCost_nonneg, canonicalThreshold_pos) live as siblings in this module.
proof idea
One-line structure instance. The three fields of TribonacciCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No tactics, no new calculation: pure packaging of already-established identities.
why it matters
Gives an inhabited certificate that the domain-cost side of the Tribonacci story is coherent: cost vanishes at perfect match, never goes negative, and the gate threshold is positive. That is the cost half of the module's STRUCTURAL THEOREM claim (zero sorry, zero axiom) tying the three-term recurrence to $D=3$ in the forcing chain (T8).
No downstream consumers are recorded yet; the natural parent is any theorem that needs a TribonacciCert witness (e.g. the sibling cert_inhabited, or later links from the three-step chain to the eight-tick octave and $\varphi$-ladder mass formula). It does not itself derive $T^3=T^2+T+1$ or identify $T$ with a power of $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.