rung_strict_ordering
plain-language theorem explainer
The theorem establishes the strict Z-rung ordering naledi below erectus below neanderthal below sapiens below the next stable rung on the recognition ladder. Paleoanthropologists and cognitive modelers working with encephalization quotients would cite it to anchor the hominin sequence within the phi-ladder. The proof is a term-mode verification that splits into four subgoals, unfolds each rung constant, and discharges the comparisons by numerical normalization.
Claim. Let the Z-rungs be the integers assigned to successive hominin species on the phi-ladder: $r_{naledi}=12$, $r_{erectus}=14$, $r_{neanderthal}=16$, $r_{sapiens}=17$, $r_{next}=19$. Then $r_{naledi} < r_{erectus} ∧ r_{erectus} < r_{neanderthal} ∧ r_{neanderthal} < r_{sapiens} ∧ r_{sapiens} < r_{next}$.
background
The module maps hominin encephalization quotients onto discrete phi-rungs of the recognition ladder, with Z-rungs drawn from the upstream Cognition.AnimalZComplexityBound structure. Each rung corresponds to a predicted EQ value obtained by scaling the human baseline by a power of phi, consistent with the mass formula and phi-ladder conventions used across Recognition Science. The local setting is Track I15 of Plan v5, which treats EQ jumps as forced by the same J-cost and defectDist mechanisms that govern atmospheric layering and nucleosynthesis tiers.
proof idea
The term proof begins with refine to split the conjunction into four separate inequalities. Each subgoal unfolds the pair of rung constants (for example rung_naledi and rung_erectus) and applies norm_num to verify the numerical order directly from their integer definitions.
why it matters
The result supplies the rung_ordering field inside eqLadderFromZRungCert, the master certificate for the encephalization ladder. It mirrors the rung_strict_ordering theorem in AtmosphericLayeringFromPhiLadder, confirming that hominin progression obeys the same strict phi-ladder ordering used for tropopause, stratopause, and thermosphere boundaries. The declaration therefore closes one link in the forcing chain from T5 J-uniqueness through T6 phi fixed point to the discrete rung structure that underlies both climate and cognitive predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.