Pith. sign in
module module moderate

IndisputableMonolith.Information.ChannelCapacity2FromJCost

show as:
view Lean formalization →

Packages the RS J-cost into a domain cost and a strictly positive canonical threshold, then exposes an inhabited certificate that the associated channel capacity equals 2. Information-side RS developments cite the certificate and the nonnegativity lemmas rather than rebuilding the cost bridge. Structure is definitional wrapping of Cost/Constants plus elementary positivity and inhabitation facts.

claimDefines a domain cost $C$ induced by the J-cost, a canonical threshold $\theta>0$, and an inhabited certificate asserting that the corresponding channel capacity equals $2$.

background

Recognition Science measures mismatch by the unique cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$), forced at T5 of the unified chain. The Cost import supplies that functional; Constants supplies the RS-native tick. Channel-capacity language in the Information domain needs a domain-level cost, a positive readout threshold, and a package that downstream proofs can inhabit rather than reconstruct.

This module is that package. It lifts $J$ to a domain cost with an evaluation identity and a nonnegativity lemma, fixes a canonical positive threshold, and records a certificate type whose inhabitant asserts capacity $2$. The value $2$ is the capacity claim being certified, not a Shannon derivation from scratch.

proof idea

Definition-and-certificate module, not a deep derivation. domainCost wraps the imported J-cost on the working domain; domainCost_at_eq and domainCost_nonneg discharge evaluation and $C\ge 0$. canonicalThreshold names the cutoff and canonicalThreshold_pos proves it is strictly positive. ChannelCap2Cert is the certificate structure; cert and cert_inhabited supply a concrete inhabitant so callers obtain capacity-$2$ as a closed package.

why it matters in Recognition Science

Moves T5 J-uniqueness from the cost layer into Information as a reusable capacity-$2$ certificate. No downstream edges are recorded yet; the inhabited cert is the intended import surface for later channel or coding arguments in the monolith. Ties RS cost geometry to capacity language without re-proving J-uniqueness. The capacity value $2$ sits near the binary structure that feeds the eight-tick octave (T7), but this module only certifies the capacity claim, it does not identify it with the octave step.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)