cert
plain-language theorem explainer
Packages three local facts (domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive) into one Shannon-entropy-max certificate. Anyone citing the RS claim that phi-rung alphabets maximize information efficiency would pull this bundle. The construction is a direct structure instance wiring three already-proved sibling lemmas.
Claim. There is a Shannon entropy maximum certificate: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
The module treats maximum Shannon entropy for an $n$-symbol alphabet, $H_{\max}=\log_2 n$ bits, in Recognition Science units. When the alphabet size sits on a golden-ratio rung, $n=\varphi^k$, one gets $H_{\max}=k\log_2\varphi\approx k\cdot 0.694$ bits. The claim is that recognition systems whose alphabets live on the $\varphi$-ladder maximize information efficiency.
The certificate structure bundles three elementary cost properties. Domain cost is the local cost functional on pairs of reals (imported from the Cost layer and Constants). The first field says cost vanishes when measure and expectation coincide (off zero). The second says cost is nonnegative for positive arguments. The third asserts that the module's canonical threshold is positive.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing (cost_nonneg: the cost of any recognition event is non-negative), via the standard $J$-cost nonnegativity at positive state.
proof idea
One-line structure instance. The three fields of ShannonEntropyMaxCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra tactics or rewriting; the def is pure field wiring.
why it matters
Gives a single named inhabitant of the Shannon-entropy-max certificate so downstream information theorems can assume the cost package without re-proving diagonal vanishing, nonnegativity, and threshold positivity. The module frames this as a structural theorem (zero sorry, zero axiom) supporting the RS story that alphabets at $\varphi$-rungs maximize bits per symbol.
No downstream consumers are recorded yet in the graph; the immediate sibling cert_inhabited is the natural next step that turns this def into an inhabited-type fact. In the broader forcing chain the cost nonnegativity side aligns with $J$-cost geometry (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$), while the $\varphi$-rung alphabet size ties to T6 ($\varphi$ as self-similar fixed point).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.