DNAStorageCert
plain-language theorem explainer
A certificate packing three structural facts for RS DNA storage density: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Information-theoretic RS work cites it as the interface that `cert` inhabits. It is a plain structure definition, not a proved theorem.
Claim. A DNA-storage certificate is a record of three properties: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats DNA storage density in Recognition Science units. Empirically one quotes Church et al. (2012) at about $2.15\times 10^{17}$ bytes/gram; RS frames the same scale as a power of $\varphi$ on the phi-ladder (structural, not a fitted constant). Status is structural: zero sorry, zero axioms.
Domain cost is the local cost functional used on this page (imported from the Cost layer). The first field demands that cost vanish when the two arguments agree and are nonzero, i.e. on the identity ray. The second field is the usual nonnegativity of cost for positive measure and expectation. The third field only asks that the module's canonical threshold sit strictly above zero.
Upstream, ObserverForcing already records that every recognition event has nonnegative cost via $J$-cost nonnegativity. The certificate reuses that pattern at the DNA-storage interface rather than re-deriving $J$.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. Inhabitation is supplied downstream by cert, which fills them with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. cert_inhabited then packages that witness as Nonempty DNAStorageCert.
why it matters
The certificate is the typed gate for the DNA storage density story in the Information domain. Downstream, cert is the concrete witness and cert_inhabited proves the type is nonempty, so later lemmas can assume a certificate without rebuilding the three inequalities.
In the broader RS forcing picture this sits far from T5–T8 (J-uniqueness, $\varphi$, eight-tick, $D=3$); it is an application-layer structural bundle that reuses cost nonnegativity and a positive threshold so density comparisons stay well-defined. It does not itself compute the $\varphi^k$ byte/gram figure; it only certifies the cost and threshold scaffolding those comparisons need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.