cert
plain-language theorem explainer
Packages three elementary properties of the DNA-storage domain cost into a single certificate record: vanishing on the diagonal, non-negativity off the axes, and positivity of the canonical threshold. Anyone citing the RS DNA-storage density module will reach for this bundle rather than the three lemmas separately. Construction is pure field assembly from already-proved sibling facts.
Claim. There exists a DNA-storage certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module treats DNA storage density in Recognition Science units. Empirically Church et al. (2012) report roughly $2.15\times 10^{17}$ bytes/gram; RS frames the same quantity as a power of $\varphi$ on the recognition ladder, with a structural (not numerical) certificate.
The domain cost is the local cost functional on matched mass/energy (or density) coordinates. Its diagonal vanishing and off-axis non-negativity mirror the global J-cost properties: $J(x)=(x+x^{-1})/2-1$ has unique minimum $0$ at $x=1$ and is non-negative for $x>0$. Upstream, cost_nonneg in ObserverForcing states that every recognition event has non-negative cost via Jcost_nonneg.
DNAStorageCert is the structure that packages exactly those three Prop fields for the DNA-storage domain. The canonical threshold is the positive cutoff used to separate admissible storage densities from the cost floor.
proof idea
One-line structure construction. The three fields of DNAStorageCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No further tactic work; the definition is pure record assembly of already-established facts.
why it matters
Gives the module a single named witness that the DNA-storage cost obeys the same non-negativity and identity-minimum pattern as the global recognition cost. Status is structural theorem (zero sorry, zero axiom). Downstream use is not yet wired (used_by empty), but the sibling cert_inhabited and any future density comparison against $\varphi^k$ bytes/gram will cite this bundle rather than re-proving the three properties. Ties the information-domain cost to the J-cost forcing chain (T5 uniqueness of $J$) without claiming a numerical match to Church et al.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.