bandwidth_monotone
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish positivity of bandwidth.
- Does not derive the explicit numerical value of the denominator.
- Does not address dynamical evolution or time dependence.
- Does not incorporate consciousness boundary costs.
formal statement (Lean)
101theorem bandwidth_monotone {A₁ A₂ : ℝ} (_h₁ : 0 < A₁) (h : A₁ ≤ A₂) :
102 bandwidth A₁ ≤ bandwidth A₂ := by
proof body
Term-mode proof.
103 unfold bandwidth
104 exact div_le_div_of_nonneg_right h (le_of_lt bandwidth_denom_pos)
105
106/-- Bandwidth scales linearly with area. -/