rung_erectus
plain-language theorem explainer
The definition assigns the natural number 14 to the Z-rung of Homo erectus on the encephalization quotient ladder. Paleoanthropologists testing hominin brain-size jumps against the recognition phi-ladder would cite this constant when checking fossil EQ ordering. It is supplied as a direct constant definition with no computation or lemmas.
Claim. The Z-rung assigned to Homo erectus is the natural number 14.
background
The module maps hominin encephalization-quotient jumps onto phi-rungs of the recognition ladder. Per the module table, H. naledi occupies rung 12 (EQ 3.5), H. erectus rung 14 (EQ 4.4), H. neanderthalensis rung 16 (EQ 5.4), and H. sapiens rung 17 (EQ 7.4). The next stable rung above sapiens is 19, identified with Z_life. These assignments rest on the Z-rung construction from Cognition.AnimalZComplexityBound and the phi-ladder mass formula yardstick times phi to the power (rung minus 8 plus gap).
proof idea
Direct definition that sets the value to the constant 14. No lemmas or tactics are applied.
why it matters
This supplies the rung value for Homo erectus required by the strict ordering theorem rung_strict_ordering and the certificate structure EQLadderFromZRungCert. It fills the slot between naledi (12) and neanderthal (16) in the hominin sequence, consistent with the eight-tick octave structure of the recognition framework. The overall ladder falsifier is any hominin EQ measurement lying outside the EQ_human times phi to the power (rung minus 17) band by a factor of two across five or more fossil samples per species.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.