Pith. sign in
module module moderate

IndisputableMonolith.Information.ChannelCapacity2FromJCost

show as:
view Lean formalization →

Package linking Shannon-style binary channel capacity to the Recognition Science J-cost. It defines a domain cost pulled back from J, a positive canonical threshold, and an inhabited certificate that the effective capacity is 2. Information theorists working in RS units would cite the certificate when tying bit capacity to the forced cost functional. The argument is definitional plus elementary nonnegativity and positivity lemmas, not a deep analytic derivation.

claimFrom the RS cost $J$, form a domain cost $C$ on the relevant ratio domain, a canonical positive threshold $\theta>0$, and a certificate asserting that the associated binary channel capacity equals $2$ (in RS-native units).

background

Recognition Science forces a unique nonnegative cost $J(x)=(x+x^{-1})/2-1$ on positive ratios (T5 in the unified forcing chain). The Cost import supplies that functional; Constants supplies the RS tick $\tau_0=1$ used to normalize discrete information steps.

This module sits in the Information domain. It pulls $J$ back to a domain cost on the channel's ratio (or likelihood) variable, records nonnegativity, and isolates a canonical positive threshold at which a binary discrimination or coding step becomes available. The certificate object packages those facts into a single inhabitance witness that the effective capacity is two distinguishable states per relevant cycle.

No external Shannon theorem is re-proved here; the point is the RS-native identification of capacity 2 with the geometry of $J$.

proof idea

Definition module with short supporting lemmas. domainCost is the pullback of $J$ to the channel domain; domainCost_at_eq and domainCost_nonneg are immediate from the corresponding properties of $J$. canonicalThreshold picks the RS scale at which the cost crosses the coding threshold; canonicalThreshold_pos is a positivity check. ChannelCap2Cert and cert package those ingredients; cert_inhabited is a one-line witness that the certificate type is nonempty.

why it matters in Recognition Science

In RS, information capacity is not an independent axiom: it must descend from the same $J$ that forces $\phi$, the eight-tick octave, and $D=3$. Capacity 2 matches the binary split natural to one tick of a two-state recognition step, consistent with the period-$2^3$ octave at the ledger level.

No downstream used_by edges are recorded in the graph snapshot, so this module currently serves as a leaf certificate in the Information layer: a reusable inhabitance fact for any later derivation that needs "channel capacity equals 2 from $J$" without reopening Cost. It closes the local gap between the cost functional and a concrete information-theoretic constant rather than advancing the T0–T8 forcing chain itself.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)