`cone_cmin_consistent`

proved

show as: view math explainer →

module: IndisputableMonolith.CPM.ConstantsAudit
domain: CPM
line: 87 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CPM.ConstantsAudit on GitHub at line 87.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  84/-! ## Consistency Verification -/
  85
  86/-- Verify that c_min is correctly computed from other constants. -/
  87theorem cone_cmin_consistent :
  88    cmin RS.coneConstants = (RS.coneConstants.Knet * RS.coneConstants.Cproj * RS.coneConstants.Ceng)⁻¹ := by
  89  rfl
  90
  91theorem eight_tick_cmin_consistent :
  92    cmin Bridge.eightTickConstants =
  93    (Bridge.eightTickConstants.Knet * Bridge.eightTickConstants.Cproj * Bridge.eightTickConstants.Ceng)⁻¹ := by
  94  rfl
  95
  96/-- Verify numerical values. -/
  97theorem cone_cmin_numerical : cmin RS.coneConstants = 1/2 := by
  98  simp only [cmin, RS.cone_Knet_eq_one, RS.cone_Cproj_eq_two, RS.cone_Ceng_eq_one]
  99  norm_num
 100
 101theorem eight_tick_cmin_numerical : cmin Bridge.eightTickConstants = 49/162 := by
 102  simp only [cmin, Bridge.eightTickConstants]
 103  norm_num
 104
 105/-! ## Probability Bounds -/
 106
 107/-- Structure for coincidence probability calculation. -/
 108structure CoincidenceBound where
 109  /-- Number of independent constants -/
 110  numConstants : ℕ
 111  /-- Precision of each match (decimal places) -/
 112  precision : ℕ
 113  /-- Upper bound on coincidence probability -/
 114  probability : ℝ
 115  /-- Proof that probability is small -/
 116  probability_small : probability < 0.01
 117

papers checked against this theorem

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