cert
plain-language theorem explainer
Packages three elementary facts about domain cost and the canonical threshold into a single certificate for eight-tick applications. Anyone citing the structural 8-tick layer (octave, SU(3) adjoint, 2^D=8) can point at this bundle rather than the three lemmas separately. The construction is a pure structure inhabitant: each field is filled by an already-proved sibling.
Claim. There is a certificate recording that (i) domain cost vanishes on the diagonal: $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) domain cost is nonnegative for positive arguments; (iii) the canonical threshold is strictly positive.
background
The module collects structural consequences of the eight-tick period $2^D=8$ forced at T7 of the unified forcing chain (musical octave, eight gluons as SU(3) adjoint, eightfold way, byte width). Status is structural: zero sorry, zero axiom.
Domain cost is the local cost functional used to compare measured and expected scales in this layer; the certificate demands it vanish when the two arguments agree and stay nonnegative when both are positive. The canonical threshold is the positive cutoff against which those costs are compared.
Upstream, nonnegativity of recognition cost is already known from ObserverForcing: any recognition event has cost $\ge 0$ via $J$-cost nonnegativity. The three field proofs here are the in-module specializations of that pattern to domain cost and the threshold.
proof idea
One-line structure inhabitant. The three fields of EightTickAppsV2Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra algebra or case split; the def is pure packaging.
why it matters
Gives a single named certificate that the cost/threshold interface for eight-tick applications is inhabited. Downstream consumers of the 8-tick layer can assume the bundle rather than re-import the three lemmas. It sits under the T7 landmark (eight-tick octave, period $2^3$) and the module's claim that all listed 8-fold phenomena descend from $2^D=8$. No used_by edges are recorded yet; the immediate sibling cert_inhabited is the natural next step that witnesses non-emptiness of the certificate type. Closes no open physics gap by itself; it is bookkeeping that keeps the structural theorem status clean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.