rung_sapiens
plain-language theorem explainer
The definition assigns the natural number 17 to the Z-rung for Homo sapiens on the encephalization-quotient ladder. Paleoanthropologists and recognition theorists cite it when mapping hominin species to phi-ladder positions for EQ predictions. It is a direct constant definition with no proof steps, directly supporting the strict rung ordering and the one-statement EQ ladder summary.
Claim. The Z-rung assigned to Homo sapiens is the natural number $17$.
background
The module maps hominin encephalization quotients onto the phi-ladder of Recognition Science. Per the module documentation, the named rungs are: H. naledi at 12 (EQ 3.5), H. erectus at 14 (EQ 4.4), H. neanderthalensis at 16 (EQ 5.4), and H. sapiens at 17 (EQ 7.4). The next stable rung above human is 19 (= Z_life), giving predicted EQ approximately 7.4 times phi squared, or 19.4.
proof idea
This declaration is a direct definition that assigns the constant value 17. No lemmas or tactics are applied.
why it matters
This definition anchors the human rung in the EQ ladder and feeds directly into EQLadderFromZRungCert, which certifies rung ordering and sets EQ_human to 7.4. It also supports eq_ladder_one_statement, which states the full ladder mapping with the next stable rung at 19 and EQ in (18.5, 20.5). In the Recognition Science framework it instantiates the phi-ladder for cognitive complexity at the T6 phi fixed point and T7 eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.