biologyInterpret
plain-language theorem explainer
biologyInterpret converts a LogicNat into its iteration count as a natural number. It supplies the interpretation step for the biological carrier in the universal forcing realization. The definition is a direct one-line application of the toNat map from the inductive LogicNat structure.
Claim. The map that sends a logic-natural number $n$ to its generation count is given by $biologyInterpret(n) := toNat(n)$, where $toNat$ counts the number of step constructors applied to the identity element in the inductive type LogicNat and Generation denotes the type of natural numbers.
background
The BiologyRealization module provides a lightweight carrier for biological realizations in which the reproductive step serves as generator and the carrier itself is the generation count. LogicNat is the inductive type forced by the Law of Logic, with identity as the zero-cost multiplicative unit and step as the generator iteration; its orbit structure mirrors the smallest subset of positive reals closed under multiplication by the generator and containing 1. The toNat function reads off the iteration depth: identity maps to 0 and each step increments the count by one. This construction sits inside the larger forcing chain that also defines generations as Fin 3 in SpectralEmergence and as an inductive type in CKM and ThreeGenerations.
proof idea
The definition is a one-line wrapper that applies the toNat function from ArithmeticFromLogic directly to the input LogicNat value.
why it matters
biologyInterpret supplies the concrete interpretation used inside biologyRealization to instantiate the LogicRealization structure with Generation as carrier and Nat as cost. It thereby links the arithmetic forced by LogicNat to the generation-count comparisons that appear downstream in the universal forcing chain. The construction aligns with the eight-tick octave and the emergence of three generations that matches the cube dimension in the spectral and physics modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.