bandwidth_monotone
plain-language theorem explainer
Recognition bandwidth increases monotonically with boundary area under the holographic constraint. Researchers deriving information throughput limits or holographic bounds in unified models would cite this monotonicity. The proof unfolds the bandwidth definition and applies the division inequality for a positive denominator.
Claim. For real numbers $A_1, A_2$ with $0 < A_1 ≤ A_2$, the recognition bandwidth satisfies $R(A_1) ≤ R(A_2)$, where $R(A) = A / (4 ℓ_P² · ln φ · 8 τ_0)$ and $k_R = ln φ$.
background
The RecognitionBandwidth module links the holographic bound on information to per-bit recognition cost $k_R = ln φ$ and the eight-tick cadence. Bandwidth is defined as area divided by (4 times Planck area times $k_R$ times eightTickCadence), yielding the maximum recognition events per unit time permitted by the bound. The upstream theorem bandwidth_denom_pos states that the denominator 4 * planckArea * k_R * eightTickCadence is positive.
proof idea
The term proof unfolds the bandwidth definition then applies div_le_div_of_nonneg_right to the area inequality, citing that the denominator is positive via bandwidth_denom_pos.
why it matters
This monotonicity result fills one of the module's listed key claims on bandwidth growth with area. It rests on the eight-tick cadence (T7) and holographic bound from the Recognition Science forcing chain. The result helps establish recognition bandwidth as the hard ceiling on ledger throughput imposed by area and per-event cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.