IndisputableMonolith.Paleoanthropology.EQLadderFromZRung
The module defines strict rung ordering for hominins on the Recognition Science phi-ladder using Z-rung inputs. Researchers modeling human evolution within the framework cite these when assigning positions to species such as naledi and sapiens. It consists of targeted definitions for each rung and associated EQ quantities together with ordering lemmas.
claimThe strict ordering of hominin rungs is expressed as $r_ {naledi} < r_{erectus} < r_{neanderthal} < r_{sapiens} < r_{next stable}$, with corresponding encephalization quotients satisfying positivity and prediction conditions derived from the phi-ladder.
background
This module sits in the paleoanthropology extension of Recognition Science and imports the base time quantum τ₀ = 1 tick along with cost functions. It introduces rung definitions for key hominin species and constructs the EQ ladder from Z-rung values.
proof idea
This is a definition module, no proofs. The argument proceeds by defining each rung explicitly from Z values and then establishing the strict inequalities between consecutive rungs via direct comparison on the phi-ladder.
why it matters in Recognition Science
The module supplies the hominin rung sequence that feeds into larger Recognition Science calculations of encephalization quotients. It realizes the application of the phi-ladder to paleoanthropological data, closing the gap between the abstract forcing chain and concrete species assignments.
scope and limits
- Does not include numerical computations of EQ for specific specimens.
- Does not extend the ladder beyond the listed hominin rungs.
- Does not derive the underlying phi-ladder or J-cost from first principles.
depends on (2)
declarations in this module (18)
-
def
rung_naledi -
def
rung_erectus -
def
rung_neanderthal -
def
rung_sapiens -
def
rung_next_stable -
theorem
rung_strict_ordering -
def
EQ_human -
theorem
EQ_human_pos -
def
EQ_predicted -
theorem
EQ_predicted_human -
theorem
EQ_predicted_pos -
theorem
EQ_below_human_mono -
def
EQ_next_stable -
theorem
EQ_next_stable_eq -
theorem
EQ_next_stable_band -
structure
EQLadderFromZRungCert -
def
eqLadderFromZRungCert -
theorem
eq_ladder_one_statement