bandwidth_times_cost_eq_rate
plain-language theorem explainer
Recognition bandwidth for positive area A satisfies bandwidth(A) multiplied by k_R times the eight-tick cadence equals the holographic bit capacity. Researchers deriving information-processing limits from the holographic principle would cite this when converting rate to capacity. The proof rewrites bandwidth as bits over cost then cancels after positivity check.
Claim. For $A > 0$, the recognition bandwidth $B(A)$ satisfies $B(A) · (k_R · T_8) = N_h(A)$, where $k_R = ln φ$ is the per-bit cost, $T_8$ the eight-tick cadence, and $N_h(A)$ the holographic bits.
background
The module introduces recognition bandwidth as the maximum rate of recognition events allowed by the holographic bound: $R_{max} = S_{holo} / (k_R · 8τ_0)$. Here $k_R = ln φ$ is the fundamental cost per ledger bit (Constants.BoltzmannConstant.k_R), replacing Boltzmann's constant in RS-native units. The eight-tick cadence is the period for one full recognition cycle (T7 in the forcing chain). holographicBits A denotes the holographic capacity $A / (4 ℓ_P^2)$ in Planck units. Upstream, k_R_pos establishes positivity of this cost, and bandwidth_eq_bits_over_cost (a sibling) encodes the division definition of bandwidth. The local setting connects five elements: holographic bound, k_R, ILG parameters, 8-tick cadence, and coherence costs.
proof idea
The proof applies the rewrite rule from bandwidth_eq_bits_over_cost to express bandwidth as holographicBits A divided by (k_R * eightTickCadence). It then proves the denominator is positive via mul_pos applied to k_R_pos and eightTickCadence_pos. Finally, div_mul_cancel₀ discharges the equality by canceling the division.
why it matters
This identity confirms that bandwidth is exactly the holographic bit rate divided by the per-event cost, closing the definition in the RecognitionBandwidth module. It directly supports the framework's unification of holographic information with the eight-tick resonance (T7) and the recognition cost k_R. No downstream uses are listed yet, but it underpins calculations of maximum ledger throughput in bounded regions. It touches the open question of how consciousness boundary costs interact with this rate limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.