all_phiInv_in_unit_interval

formal source

 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]
 117    -- Goal: 1 * φ < 1 * φ³, i.e., φ < φ³
 118    have h2 : phi^2 = phi + 1 := phi_sq_eq
 119    nlinarith [one_lt_phi, hpos, h2]
 120
 121structure PhiInverseInvariantsCert where
 122  phiInv_pos : 0 < phiInv
 123  phiInv_lt_one : phiInv < 1
 124  phiInv_lt_phi : phiInv < phi
 125  fib_identity : phiInv = phi - 1
 126  inv_sq_identity : 1 / phi^2 = 2 - phi
 127  inv_cubed_identity : 1 / phi^3 = 2 * phi - 3
 128  five_instances_equal :
 129    senolyticTargetRatio = giniCeiling ∧
 130    giniCeiling = policyBalance ∧
 131    policyBalance = stemCellDecay ∧
 132    stemCellDecay = circadianDecay
 133  cabibbo_smaller : 0 < cabibboFactor ∧ cabibboFactor < phiInv
 134
 135noncomputable def phiInverseInvariantsCert : PhiInverseInvariantsCert where