cf_below_bond
plain-language theorem explainer
The theorem establishes that the counterfactual floor rung at 5 lies strictly below the bond rung at 8 on the Z-complexity ladder. Researchers modeling animal cognition thresholds in Recognition Science cite it to anchor the initial segment of the structural ordering. The proof reduces to unfolding the two constant definitions and applying numerical normalization.
Claim. Let $z_{cf}$ denote the counterfactual-floor rung and $z_{bond}$ the bond rung on the Z-complexity ladder. Then $z_{cf} < z_{bond}$, i.e., $5 < 8$.
background
The Animal Z-Complexity Bound module defines the Z-complexity ladder as a geometric sequence indexed by integer rung $k$, with structurally significant thresholds including the bond rung at $k=8$ (threshold for sustained molecular recognition) and the counterfactual-floor rung at $k=5$ (floor for counterfactual reasoning, matching $Z_{cf} = phi^5$). The module documentation states that the ladder is well-defined and strictly increasing, with named rungs ordered as bond < cf-floor < vertebrate < octopus < cetacean < human.
proof idea
The proof is a one-line wrapper that unfolds the definitions of z_rung_cf and z_rung_bond to the constants 5 and 8, then applies norm_num to verify the inequality.
why it matters
This theorem supplies the base inequality for the rung_ordering result and the cognition_floor_below_bond_z and cognition_floor_below_human_z theorems in the same module. It fills the first link in the strict ordering of the phi-ladder for animal cognition, consistent with the eight-tick octave and phi-ladder construction from the forcing chain (T5-T8). It touches the open question of empirical rung assignments without claiming mechanistic derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.