EightTickAppsV2Cert
plain-language theorem explainer
A certificate packing three elementary facts about the eight-tick application layer: the domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Downstream code cites the inhabited instance rather than the bare structure. The declaration is pure data: three Prop fields with no proof body.
Claim. A certificate consists of three statements: (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 collects structural consequences of the eight-tick octave forced by $2^D=8$ (T7 in the forcing chain, with $D=3$ from T8). It lists familiar octets (musical notes, color-spin quark count, SU(3) gluons, Gell-Mann eightfold way, byte width) as applications of that period, not as independent postulates.
domainCost is the local cost functional on pairs of positive reals used by the application layer; the certificate only records that it vanishes when the two arguments agree and stays nonnegative off the diagonal. canonicalThreshold is the positive cutoff against which those costs are compared.
Upstream, ObserverForcing already proves that every recognition-event cost is nonnegative via the J-cost minimum at identity. The present fields are the analogous elementary positivity and normalization facts for the eight-tick domain cost, not a re-derivation of J-uniqueness (T5) or the Recognition Composition Law.
proof idea
No proof body: the declaration is a structure type whose three fields are propositions. Inhabitation is supplied separately by the definition cert, which fills the fields with the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The theorem cert_inhabited then packages that definition as Nonempty EightTickAppsV2Cert.
why it matters
Gives a single named bundle that downstream eight-tick application code can require instead of three loose lemmas. The module marks itself a structural theorem (zero sorry, zero axiom); this certificate is the interface that makes that claim checkable.
Parents are the local inhabitant cert and the nonemptiness theorem cert_inhabited. The content sits under the T7 eight-tick octave and the broader forcing chain, but does not itself force $\phi$, $D=3$, or the J-cost; it only packages positivity and diagonal vanishing for the application-layer cost. No open scaffold is attached: claim status is definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.