bandwidth_denom_pos
plain-language theorem explainer
Positivity of the denominator in the recognition bandwidth formula follows from the positivity of Planck area, the recognition cost per bit, and the eight-tick cadence. Researchers modeling information throughput under holographic bounds cite this result to guarantee that the maximum recognition rate remains well-defined. The proof applies the multiplication-positivity lemma three times and discharges each factor via its dedicated positivity theorem.
Claim. $0 < 4 · ℓ_P² · ln(φ) · 8τ₀$, where ℓ_P² is the Planck area, ln(φ) is the recognition cost per bit, and 8τ₀ is the eight-tick cadence period.
background
The RecognitionBandwidth module defines recognition bandwidth as the maximum rate of recognition events inside a holographically bounded region: R_max = A / (4ℓ_P² · ln(φ) · 8τ₀). This expression combines the holographic entropy bound (information capacity proportional to boundary area over four Planck areas) with the per-bit recognition cost k_R = ln(φ) and the eight-tick cadence required by the forcing chain.
proof idea
The term proof applies mul_pos three times to reduce the four-factor product inequality to separate positivity claims on each factor. It then invokes linarith on planckArea_pos and exact applications of k_R_pos and eightTickCadence_pos to close the subgoals.
why it matters
This result is the immediate prerequisite for the parent theorems bandwidth_pos and bandwidth_monotone, which establish that recognition bandwidth is positive and increases with boundary area. It supplies the missing positivity link between the holographic bound, the RS Boltzmann constant k_R = ln(φ), and the eight-tick cadence (T7) in the forcing chain, confirming that the hard ceiling on ledger throughput is strictly positive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.