bandwidth_pos
plain-language theorem explainer
Recognition bandwidth is strictly positive for any positive boundary area. Analysts deriving information processing bounds or critical loading thresholds in holographic regions cite this result to ensure positive throughput. The proof applies the division positivity lemma directly to the area hypothesis and the established positivity of the formula's denominator.
Claim. If the boundary area satisfies $A > 0$, then the recognition bandwidth satisfies $0 < R_{max}(A)$, where $R_{max}(A) = A / (4 ell_P^2 cdot ln(phi) cdot 8 tau_0)$.
background
The Recognition Bandwidth module connects five elements of Recognition Science: the holographic bound on information, recognition cost per bit $k_R = ln phi$, ILG parameters, the 8-tick cadence, and consciousness boundary cost. It defines recognition bandwidth as the maximum rate of recognition events permitted by the holographic bound: $R_{max}(A) = A / (4 ell_P^2 cdot k_R cdot 8 tau_0)$. This supplies a hard ceiling on ledger throughput imposed by area and per-bit cost.
proof idea
The proof is a one-line wrapper that applies the div_pos lemma to the hypothesis that the area is positive together with the theorem bandwidth_denom_pos establishing positivity of the denominator.
why it matters
This positivity result is required by the BernsteinBound structure to guarantee positive derivative bounds and by the loadRatio_pos theorem to obtain positive load ratios. It fills the first key result listed in the module documentation, supporting the hard ceiling on ledger throughput from the holographic bound and eight-tick cadence in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.