cert_inhabited
plain-language theorem explainer
Existence of an AgeGradingCert is established by exhibiting the concrete witness cert that meets the grade-count, positivity, and proximity conditions. Anthropologists modeling universal human life-stage divisions cite this to anchor the five-grade pattern predicted by configDim D equals 5. The argument is a direct term construction that packs the pre-verified cert into the Nonempty type.
Claim. There exists a certificate $C$ such that the number of age grades equals 5, the adolescence-to-childhood ratio is positive, and the absolute deviation of that ratio from $phi$ is less than 0.1.
background
AgeGradingCert is the structure whose fields require ageGradeCount to equal 5, adolescenceChildhoodRatio to be positive, and the absolute difference between adolescenceChildhoodRatio and phi to lie below 0.1. The surrounding module derives these constraints from the Recognition Science claim that configDim D equals 5, the same template that produces five Big Five factors, five Köppen zones, and five sleep stages. The upstream structure definition supplies the precise predicates that the certificate must satisfy.
proof idea
The proof is a one-line term that applies the structure constructor to the pre-defined cert witness.
why it matters
This declaration closes the existence claim for the five-grade certificate inside the Anthropology module, confirming that the structural theorem for age-grading systems is inhabited. It supports the broader Recognition Science prediction that configDim D equals 5 forces the observed modal count of five grades with ratios near phi. The module-level falsifier remains any ethnographic survey of at least 100 cultures whose modal age-grade count lies outside 5 plus or minus 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.