`bandwidth_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Unification.RecognitionBandwidth
domain: Unification
line: 93 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Unification.RecognitionBandwidth on GitHub at line 93.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  90  · exact eightTickCadence_pos
  91
  92/-- Recognition bandwidth is positive for positive area. -/
  93theorem bandwidth_pos {A : ℝ} (hA : 0 < A) : 0 < bandwidth A :=
  94  div_pos hA bandwidth_denom_pos
  95
  96/-- Alias for bandwidth_pos. -/
  97theorem bandwidth_pos' {A : ℝ} (hA : 0 < A) : 0 < bandwidth A :=
  98  bandwidth_pos hA
  99
 100/-- Bandwidth is monotone in area: larger boundary → more throughput. -/
 101theorem bandwidth_monotone {A₁ A₂ : ℝ} (_h₁ : 0 < A₁) (h : A₁ ≤ A₂) :
 102    bandwidth A₁ ≤ bandwidth A₂ := by
 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. -/
 107theorem bandwidth_linear (A c : ℝ) (_hc : 0 < c) :
 108    bandwidth (c * A) = c * bandwidth A := by
 109  unfold bandwidth
 110  ring
 111
 112/-! ## §3. Holographic Capacity Recovery -/
 113
 114/-- The total holographic capacity (bits) of area A. -/
 115noncomputable def holographicBits (area : ℝ) : ℝ :=
 116  area / (4 * planckArea)
 117
 118/-- Bandwidth equals holographic bits divided by (k_R · 8τ₀). -/
 119theorem bandwidth_eq_bits_over_cost {A : ℝ} (_hA : 0 < A) :
 120    bandwidth A = holographicBits A / (k_R * eightTickCadence) := by
 121  unfold bandwidth holographicBits
 122  ring
 123

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.