def
definition
senolyticTargetRatio
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CrossDomain.PhiInverseInvariants on GitHub at line 80.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
77/-! ## Domain instances. -/
78
79/-- Senolytic target ratio. -/
80noncomputable def senolyticTargetRatio : ℝ := phiInv
81
82/-- Gini ceiling (RS prediction). -/
83noncomputable def giniCeiling : ℝ := phiInv
84
85/-- Counter-cyclical policy balance. -/
86noncomputable def policyBalance : ℝ := phiInv
87
88/-- Stem-cell reserve decay per phi-rung. -/
89noncomputable def stemCellDecay : ℝ := phiInv
90
91/-- Amplitude decay per circadian aging rung. -/
92noncomputable def circadianDecay : ℝ := phiInv
93
94/-- Cabibbo mixing angle factor. -/
95noncomputable def cabibboFactor : ℝ := 1 / phi^3
96
97/-- All five 1/φ instances are equal. -/
98theorem all_phiInv_instances_equal :
99 senolyticTargetRatio = giniCeiling ∧
100 giniCeiling = policyBalance ∧
101 policyBalance = stemCellDecay ∧
102 stemCellDecay = circadianDecay := ⟨rfl, rfl, rfl, rfl⟩
103
104/-- All five are bounded in (0, 1). -/
105theorem all_phiInv_in_unit_interval :
106 0 < senolyticTargetRatio ∧ senolyticTargetRatio < 1 := ⟨phiInv_pos, phiInv_lt_one⟩
107
108/-- Cabibbo factor is in (0, 1) (smaller than phiInv). -/
109theorem cabibbo_in_unit : 0 < cabibboFactor ∧ cabibboFactor < phiInv := by
110 unfold cabibboFactor phiInv