ShannonEntropyMaxCert
plain-language theorem explainer
Certificate packing three structural hypotheses for the RS Shannon-entropy maximum: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Information theorists working the phi-rung alphabet cite it when assembling H_max = k log2(phi). Pure structure definition; inhabitance is discharged separately by the concrete cert.
Claim. A Shannon-entropy-maximum certificate is a triple of facts: (i) the domain cost satisfies $C(r,r)=0$ for every nonzero real $r$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $\tau$ obeys $\tau>0$.
background
The module treats maximum Shannon entropy for an $n$-symbol alphabet, $H_{\max}=\log_2 n$ bits, specialized to Recognition Science alphabets whose size sits on a phi-rung: $n=\varphi^k$ yields $H_{\max}=k\log_2\varphi\approx k\cdot 0.694$ bits. Recognition systems at those rungs are claimed to maximize information efficiency.
Domain cost $C(m,e)$ is the local cost functional on positive reals used in place of a raw Shannon sum; the sibling lemmas establish $C(r,r)=0$ off zero and $C\ge 0$ on the positive quadrant. The canonical threshold is the positive cutoff against which efficiency comparisons are made. Upstream, ObserverForcing records that every recognition-event cost is nonnegative via the J-cost minimum at identity ($x=1$), which licenses the nonnegativity field here.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity on positive arguments, positivity of the canonical threshold). Inhabitance is supplied later by the concrete cert record, which wires in the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the typed interface that the module's concrete certificate and its Nonempty witness inhabit. Downstream, cert fills the three fields from the sibling cost and threshold lemmas, and cert_inhabited packages that as Nonempty ShannonEntropyMaxCert, closing the structural theorem (0 sorry, 0 axiom) advertised in the module header.
In the broader RS chain this sits on the information side of the phi-ladder: once alphabets are forced to sizes $\varphi^k$ (T6 self-similarity), the max-entropy figure becomes $k\log_2\varphi$, tying Shannon capacity to the same golden ratio that appears in the mass ladder and the eight-tick octave. The certificate isolates exactly the cost axioms needed before any numerical entropy comparison is stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.