cert
plain-language theorem explainer
Packages three structural facts into the RS bandwidth-phi certificate: domain cost vanishes on equal nonzero arguments, is nonnegative for positive inputs, and the canonical threshold is positive. Cited by anyone specializing Shannon capacity at phi-resonance (SNR = phi^3). Construction is a pure structure fill from three sibling lemmas.
Claim. There is an RS bandwidth-$\phi$ certificate consisting of: (i) for every $r \neq 0$, the domain cost of $(r,r)$ is zero; (ii) for all $m,e > 0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module specializes Shannon channel capacity $C = B \log_2(1+\mathrm{SNR})$ to Recognition Science at $\phi$-resonance. There the signal-to-noise ratio is forced to $\phi^D = \phi^3 \approx 4.24$ ($6.27,\mathrm{dB}$), so $C_{\mathrm{RS}} = B \log_2(\phi^3+1) = B \log_2(5.24) \approx B \cdot 2.39$ bits/Hz. Status is structural (no sorry, no axioms).
domainCost is the local cost functional on measure/energy pairs; the certificate demands it vanish on the diagonal $m=e$ (nonzero) and stay nonnegative off it. canonicalThreshold is the positive cutoff used to mark the resonance band. Upstream, nonnegativity of recognition cost is already known from ObserverForcing (cost_nonneg: every recognition event has $J$-cost $\ge 0$), which underwrites the domain-cost nonnegativity field.
proof idea
Pure structure construction. The three fields of BandwidthPhiCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional tactics or algebraic work; the definition is the inhabited certificate object itself.
why it matters
Gives a single named witness that the cost and threshold hypotheses needed for the RS bandwidth-$\phi$ specialization hold. That specialization is the structural claim of the module: Shannon capacity evaluated at the forced SNR $\phi^3$ (from $D=3$ in the forcing chain T8 and the golden ratio fixed by T5/T6). Downstream use is currently empty in the graph, but the sibling cert_inhabited and any capacity or band-limit theorems in Information will consume this bundle rather than re-prove the three facts. Closes the certificate interface for the structural bandwidth result without introducing axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.