AgeGradingCert
plain-language theorem explainer
AgeGradingCert packages the claim that human societies exhibit five age grades with the childhood-to-adolescence boundary ratio positive and within 0.1 of the golden ratio. Anthropologists and Recognition Science theorists cite it to connect ethnographic patterns to the configDim = 5 prediction. The structure is a direct record bundling three field assertions taken from the module constants ageGradeCount and adolescenceChildhoodRatio.
Claim. A structure $C$ such that the grade count field asserts the number of age grades equals 5, the ratio positivity field asserts $0 < r$ where $r$ is the adolescence-to-childhood boundary ratio, and the ratio-near-phi field asserts $|r - phi| < 0.1$.
background
The module establishes age-grading systems as a universal cultural pattern with exactly five grades (childhood, adolescence, adulthood, middle age, old age) forced by configDim D = 5, the same template that yields five Big Five factors, five Köppen zones, and five sleep stages. The life-span ratios between adjacent grades are predicted to scale near phi, with the explicit childhood-to-adolescence example given as 20/12 ≈ 1.67. ageGradeCount is the constant natural number 5 that encodes the modal count across cultures. adolescenceChildhoodRatio is the real number 20/12 that encodes the boundary ratio and is asserted to lie near phi.
proof idea
The declaration is a structure definition whose three fields directly reference the module constants ageGradeCount and adolescenceChildhoodRatio. No lemmas or tactics are invoked; the object is assembled by naming the equality ageGradeCount = 5 together with the two inequalities on adolescenceChildhoodRatio.
why it matters
AgeGradingCert supplies the certificate object that is instantiated by the downstream definition cert and discharged by the theorem cert_inhabited proving Nonempty AgeGradingCert. It completes one concrete instance of the structural theorem that five-fold divisions arise from configDim D = 5 inside the Recognition Science framework, parallel to the eight-tick octave and D = 3 spatial dimensions. The construction touches the open ethnographic question whether the phi-scaling of age boundaries remains stable across large cross-cultural samples.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.