def
definition
giniCeiling
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Economics.InequalityCeilingFromSigma on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25open Constants Cost
26
27/-- The Gini ceiling = 1/φ (golden ratio reciprocal). -/
28noncomputable def giniCeiling : ℝ := phi⁻¹
29
30/-- 1/φ = φ - 1 (golden ratio identity: φ² = φ + 1 → φ - 1 = 1/φ). -/
31theorem giniCeiling_eq_phi_minus_one : giniCeiling = phi - 1 := by
32 unfold giniCeiling
33 have h := phi_sq_eq
34 field_simp [phi_ne_zero]
35 linarith [phi_sq_eq]
36
37/-- Gini ceiling in (0.617, 0.622). -/
38theorem giniCeiling_in_band :
39 (0.617 : ℝ) < giniCeiling ∧ giniCeiling < 0.623 := by
40 unfold giniCeiling
41 have h1 := phi_gt_onePointSixOne
42 have h2 := phi_lt_onePointSixTwo
43 constructor
44 · rw [lt_inv_comm₀ (by norm_num) phi_pos]
45 linarith
46 · rw [inv_lt_comm₀ phi_pos (by norm_num)]
47 linarith
48
49/-- J(1/φ) = J(φ) (symmetry). -/
50theorem gini_jcost_symmetric : Jcost giniCeiling = Jcost phi := by
51 unfold giniCeiling
52 exact (Jcost_symm phi_pos).symm
53
54structure InequalityCeilingCert where
55 gini_eq : giniCeiling = phi - 1
56 gini_band : (0.617 : ℝ) < giniCeiling ∧ giniCeiling < 0.623
57 gini_jcost : Jcost giniCeiling = Jcost phi
58