TribonacciCert
plain-language theorem explainer
Packages three structural axioms for the RS domain-cost model tied to the Tribonacci constant at D=3: diagonal vanishing, nonnegativity for positive mass/energy, and a positive canonical threshold. Downstream code cites it to obtain a concrete inhabited certificate. The declaration is a pure structure interface with no proof body.
Claim. A Tribonacci certificate is a record of three properties: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is 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 treats the Tribonacci constant $T\approx 1.839$ defined by $T^3=T^2+T+1$ as the structural growth ratio of a three-term recognition recurrence at spatial dimension $D=3$. The text notes that $T$ is not simply $\varphi^{D-1}$ or $\varphi^{3/2}$; the link is structural rather than a direct golden-ratio power.
domainCost is the local cost functional on pairs of positive reals (mass/energy style arguments). The diagonal identity domainCost r r = 0 for $r\neq 0$ encodes perfect self-match. Nonnegativity mirrors the global J-cost fact that every recognition event has cost $\ge 0$ (ObserverForcing: "The cost of any recognition event is non-negative").
canonicalThreshold is the positive cutoff used to separate admissible Tribonacci-scale comparisons from the zero-cost diagonal. The structure only names these three Prop fields; sibling lemmas supply the actual proofs.
proof idea
No proof body: this is a structure declaration. It declares three fields of type Prop (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). 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 cost axioms needed by the Tribonacci layer of the foundation. Downstream, cert builds a concrete value of this structure, and cert_inhabited records Nonempty TribonacciCert, closing the structural theorem status claimed in the module doc (0 sorry, 0 axiom).
In the broader RS chain this sits under the D=3 forcing (T8) and the three-term recurrence that the module associates with recognition at that dimension. It does not itself force $T$ or derive particle masses; it only certifies the cost-side hypotheses those later steps may assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.