def
definition
policyBalance
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CrossDomain.PhiInverseInvariants on GitHub at line 86.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
111 refine ⟨?_, ?_⟩
112 · exact div_pos one_pos (pow_pos phi_pos 3)
113 · -- 1/φ³ < 1/φ since φ³ > φ when φ > 1
114 have hpos := phi_pos
115 have hp3 := pow_pos phi_pos 3
116 rw [div_lt_div_iff₀ hp3 hpos]