def
definition
ageGradeCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Anthropology.AgeGradingFromConfigDim on GitHub at line 39.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
36noncomputable section
37
38/-- Five universal age grades. -/
39def ageGradeCount : ℕ := 5
40
41theorem ageGradeCount_eq : ageGradeCount = 5 := rfl
42
43theorem ageGradeCount_pos : 0 < ageGradeCount := by
44 rw [ageGradeCount_eq]; norm_num
45
46/-- Adolescence/childhood age boundary ratio ≈ φ. -/
47def adolescenceChildhoodRatio : ℝ := 20 / 12
48
49theorem adolescenceChildhoodRatio_pos : 0 < adolescenceChildhoodRatio := by
50 unfold adolescenceChildhoodRatio; norm_num
51
52/-- This ratio is close to φ: 20/12 ≈ 1.667 and φ ≈ 1.618. -/
53theorem adolescenceChildhoodRatio_near_phi :
54 |adolescenceChildhoodRatio - phi| < 0.05 + 0.05 := by
55 unfold adolescenceChildhoodRatio
56 have h1 : (1.61 : ℝ) < phi := phi_gt_onePointSixOne
57 have h2 : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
58 rw [abs_lt]
59 constructor <;> norm_num <;> linarith
60
61structure AgeGradingCert where
62 grade_count : ageGradeCount = 5
63 ratio_pos : 0 < adolescenceChildhoodRatio
64 ratio_near_phi : |adolescenceChildhoodRatio - phi| < 0.05 + 0.05
65
66noncomputable def cert : AgeGradingCert where
67 grade_count := ageGradeCount_eq
68 ratio_pos := adolescenceChildhoodRatio_pos
69 ratio_near_phi := adolescenceChildhoodRatio_near_phi