IndisputableMonolith.Information.LDPCCodeRateFromJCost
Connects LDPC code-rate bounds to the Recognition Science J-cost on positive reals. Defines a domain cost, its equilibrium value and nonnegativity, a positive canonical threshold, and an LDPC certificate type with an inhabited instance. Coding theorists linking sparse parity-check ensembles to the RS cost functional would cite it. Mostly definitional scaffolding with elementary positivity and equilibrium lemmas.
claimOn the positive reals, a domain cost $C$ is built from the J-cost $J(x)=(x+x^{-1})/2-1$. At equilibrium $C$ vanishes; elsewhere $C\ge 0$. A canonical threshold $\theta>0$ is fixed from this cost. An LDPC certificate packages rate data relative to $\theta$, and at least one such certificate exists.
background
Recognition Science forces a unique symmetric cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) via the Recognition Composition Law and the T5 uniqueness step. The Cost import supplies that functional; Constants supplies the RS tick scale used when rates are expressed in native units.
This Information-domain module treats LDPC (low-density parity-check) code rate as a quantity to be compared against a J-derived cost on a positive real domain. The sibling objects introduce a domain cost, record that it is zero at equilibrium and nonnegative in general, and fix a strictly positive canonical threshold against which certificate data are judged.
The LDPC certificate type is the module's main packaging device: it bundles the numerical rate-side data needed to assert that a sparse parity-check ensemble clears the J-cost threshold.
proof idea
Definition-heavy module. Domain cost is introduced from $J$; equilibrium vanishing and nonnegativity are short lemmas from the standard properties of $J$ (minimum $0$ at $x=1$). The canonical threshold is a positive constant extracted from that cost; positivity is immediate. The certificate structure is a data type with an inhabited instance, so downstream code can pick a default witness without constructing one by hand. No deep coding-theoretic existence proof lives here; the argument is algebraic bookkeeping around $J$.
why it matters in Recognition Science
Places LDPC rate language inside the RS cost calculus so information-theoretic bounds can be stated in the same units as the forcing chain (T5 J-uniqueness and the RCL). Downstream graph edges are empty in the current mirror, so this module is a leaf: it prepares certificate and threshold vocabulary rather than discharging a named parent theorem. It is the natural hook for later claims that sparse-graph code rates sit above or below the J-derived canonical threshold, and for any bridge from channel coding to the eight-tick / phi-ladder bookkeeping used elsewhere in the monolith.
scope and limits
- Does not prove Shannon capacity or any ensemble-averaged LDPC threshold theorem.
- Does not construct explicit parity-check matrices or decode algorithms.
- Does not derive J from the RCL; it consumes J from Cost.
- Does not claim a numerical match to measured code rates without further hypotheses.
- Does not feed a recorded downstream theorem in the current dependency graph.