AnimalZComplexityBoundCert
plain-language theorem explainer
The AnimalZComplexityBoundCert structure bundles five properties of the Z-complexity ladder: geometric growth with ratio phi, strict monotonicity, the rung ordering cf < bond < vertebrate < octopus < cetacean < human < life, and the cognition floor fixed at phi^5. Researchers working on Recognition Science models of animal cognition cite it to anchor the phi-ladder assignments in arc 10c. It is realized as a plain structure definition that packages the properties with no additional proof steps required.
Claim. A certificate asserting that the function $Z(k) := phi^k$ satisfies $Z(0)=1$, $Z(k+1)=phi Z(k)$ for all $k in mathbb{N}$, $Z(k)<Z(k+1)$ for all $k$, the strict ordering $Z_5 < Z_8 < Z_{12} < Z_{14} < Z_{15} < Z_{17} < Z_{19}$, and the cognition floor equals $phi^5$.
background
The Z-rung function is defined by $z_rung(k) := Constants.phi^k$, so every rung is positive and the sequence is geometric. Named rungs are fixed integers: $z_rung_cf := 5$, $z_rung_bond := 8$, $z_rung_vertebrate := 12$, $z_rung_octopus := 14$, $z_rung_cetacean := 15$, $z_rung_human := 17$, with the life rung at 19. The cognition floor is the separate definition $z_cognition_floor := z_rung(z_rung_cf)$. Module context places this in the phi-ladder of animal cognition (arc 10c), where the bond rung marks sustained molecular recognition and the life rung marks self-sustaining biological recognition.
proof idea
This is a structure definition that directly encodes the five listed fields. The geometric and monotonicity properties follow from the upstream definition of z_rung together with the theorems z_rung_zero, z_rung_succ and z_rung_strictly_increasing. The rung_ordering field is supplied by the upstream theorem of the same name. The cognition_floor_eq field is supplied by the upstream definition z_cognition_floor_eq.
why it matters
It supplies the master certificate for arc 10c, the cognition seed of the animal Z-complexity bound. The downstream definition animalZComplexityBoundCert inhabits the structure by supplying concrete proofs for each field. The construction formalizes the phi-ladder forced at T6 and the eight-tick octave, providing the structural anchor for placing empirical cognitive milestones without claiming mechanistic derivation of the rung numbers themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.