theorem
proved
phiInvCubed_eq_two_phi_minus_three
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.CrossDomain.PhiInverseInvariants on GitHub at line 69.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
66 linarith [hkey]
67
68/-- 1/φ³ = 2φ - 3 (= the Cabibbo-angle factor). -/
69theorem phiInvCubed_eq_two_phi_minus_three : 1 / phi^3 = 2 * phi - 3 := by
70 have hpos : phi^3 ≠ 0 := ne_of_gt (pow_pos phi_pos 3)
71 have hsq : phi^2 = phi + 1 := phi_sq_eq
72 have h3 : phi^3 = 2 * phi + 1 := phi_cubed_eq
73 have hkey : phi^3 * (2 * phi - 3) = 1 := by nlinarith [hsq, h3]
74 rw [eq_comm, eq_div_iff hpos]
75 linarith [hkey]
76
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 ∧