gap_pos
plain-language theorem explainer
The theorem establishes that the gap to Shannon capacity remains strictly positive for every positive real block length N under the φ-suppression model. Information theorists and LDPC code designers cite it to anchor the positivity half of the rate certificate. The proof is a direct term-mode reduction that unfolds the definition and applies the standard positivity rules for reciprocals and products.
Claim. For every real number $N > 0$, the gap to capacity satisfies $1/ (φ N) > 0$.
background
The module develops the φ-suppressed gap-to-capacity for LDPC codes, where the finite-N correction to Shannon capacity is 1/(φN). The upstream definition states gapToCapacity (N : ℝ) : ℝ := 1 / (phi * N), supplying the explicit form used throughout the certificate. This sits inside the Recognition Science derivation of information bounds from the J-cost functional and the Recognition Composition Law, with phi the self-similar fixed point forced at T6.
proof idea
The term-mode proof unfolds gapToCapacity to expose 1/(phi * N). It applies one_div_pos.mpr to convert the goal into the equivalent statement phi * N > 0. The final step closes with mul_pos applied to the known positivity of phi and the hypothesis 0 < N.
why it matters
This result supplies the positivity component of LDPCRateCert, which is consumed by LatticeState in the ethics module (where spectral_gap > 0 is required) and by TurbineGeometry in flight applications. It directly supports the module's claim that the gap follows g(N) = 1/(φN) and remains positive, feeding the monotone-decreasing and doubling-halves siblings. It touches the open empirical question of stable gap behavior across corpora of at least 100 LDPC codes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.