ageGradeCount_pos
plain-language theorem explainer
The theorem establishes positivity of the universal age-grade count in human societies. Anthropologists and cultural modelers would cite it to anchor the claim of exactly five grades as a structural universal. The proof is a one-line wrapper that rewrites via the defining equality and normalizes the resulting numerical inequality.
Claim. $0 < 5$, where 5 is the fixed count of universal age grades (childhood through old age) forced by configDim $D=5$.
background
The module models age-grading systems as a Recognition Science universal, with most cultures recognizing exactly five grades: childhood (0-12 yr), adolescence (12-20 yr), adulthood (20-45 yr), middle age (45-65 yr), and old age (65+ yr). The life-span ratios between adjacent grades scale near powers of phi, consistent with the self-similar fixed point in the forcing chain. The local setting is the structural theorem that five grades are forced by configDim $D=5$, the same template used for Big Five factors, Koppen zones, sleep stages, and social strata.
proof idea
The proof is a one-line wrapper. It first applies the equality theorem ageGradeCount_eq to replace ageGradeCount with the literal 5, then invokes norm_num to discharge the concrete inequality 0 < 5.
why it matters
This result supplies the elementary positivity fact required by the module's structural claim that five age grades are universal. It directly supports the RS prediction that configDim $D=5$ forces the same count across anthropology, personality, climate, and sleep domains. The module falsifier is any ethnographic survey of at least 100 cultures showing a modal count reliably outside 5 plus or minus 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.