`giniCeiling`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.PhiInverseInvariants
domain: CrossDomain
line: 83 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.PhiInverseInvariants on GitHub at line 83.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
 111  refine ⟨?_, ?_⟩
 112  · exact div_pos one_pos (pow_pos phi_pos 3)
 113  · -- 1/φ³ < 1/φ since φ³ > φ when φ > 1

papers checked against this theorem

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