theorem proved term proof

`bandwidth_times_cost_eq_rate`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 126theorem bandwidth_times_cost_eq_rate {A : ℝ} (hA : 0 < A) :
 127    bandwidth A * (k_R * eightTickCadence) = holographicBits A := by

proof body

Term-mode proof.

 128  rw [bandwidth_eq_bits_over_cost hA]
 129  have h : 0 < k_R * eightTickCadence := mul_pos k_R_pos eightTickCadence_pos
 130  exact div_mul_cancel₀ (holographicBits A) (ne_of_gt h)
 131
 132/-! ## §4. Connection to ILG Parameters -/
 133
 134/-- ILG coherence energy C_lag = φ⁻⁵ equals the coherence exponent E_coh.
 135    This is the energy quantum per recognition event in RS-native units. -/

depends on (17)

Lean names referenced from this declaration's body.

k_R in IndisputableMonolith.Constants.BoltzmannConstant decl_use
k_R_pos in IndisputableMonolith.Constants.BoltzmannConstant decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
C_lag in IndisputableMonolith.Gravity.EightTickResonance decl_use
k_R in IndisputableMonolith.Gravity.UltramassiveBH decl_use
k_R_pos in IndisputableMonolith.Gravity.UltramassiveBH decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
bandwidth in IndisputableMonolith.Unification.RecognitionBandwidth decl_use
bandwidth_eq_bits_over_cost in IndisputableMonolith.Unification.RecognitionBandwidth decl_use
eightTickCadence in IndisputableMonolith.Unification.RecognitionBandwidth decl_use
eightTickCadence_pos in IndisputableMonolith.Unification.RecognitionBandwidth decl_use
holographicBits in IndisputableMonolith.Unification.RecognitionBandwidth decl_use