`bandwidth`

definition

show as: view math explainer →

module: IndisputableMonolith.Unification.RecognitionBandwidth
domain: Unification
line: 74 · 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 74.

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

  71    - Holographic capacity: A/(4ℓ_P²)      [from Quantum.HolographicBound]
  72    - Per-bit cost: k_R = ln(φ)            [from Constants.BoltzmannConstant]
  73    - Processing rate: 8τ₀ per cycle       [from Foundation.EightTick]  -/
  74noncomputable def bandwidth (area : ℝ) : ℝ :=
  75  area / (4 * planckArea * k_R * eightTickCadence)
  76
  77/-- Planck area is positive. -/
  78theorem planckArea_pos : 0 < planckArea := by
  79  unfold planckArea planckLength
  80  positivity
  81
  82/-- The denominator of the bandwidth formula is positive. -/
  83theorem bandwidth_denom_pos : 0 < 4 * planckArea * k_R * eightTickCadence := by
  84  apply mul_pos
  85  apply mul_pos
  86  apply mul_pos
  87  · linarith [planckArea_pos]
  88  · exact planckArea_pos
  89  · exact k_R_pos
  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)

papers checked against this theorem

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