biology_arith_equiv_nat
plain-language theorem explainer
The definition supplies an equivalence between the Peano carrier extracted from the arithmetic object of the biological realization and the logic-forced natural numbers. Researchers mapping generation counts into the universal forcing structure would cite it to confirm that the reproductive-step generator produces the same orbit as the Law of Logic. It is realized as a direct one-line wrapper that invokes the orbit equivalence field already present in the biology realization.
Claim. Let $R$ be the biological realization whose carrier is the set of generations with the reproductive step as generator. The carrier of the Peano arithmetic structure extracted from the arithmetic object of $R$ is equivalent to the logic-natural numbers, the inductive type generated by an identity element and a successor that mirrors the orbit under repeated multiplication by the generator.
background
The module defines a lightweight biological realization in which the carrier is generation count and the cost is the natural numbers, with the reproductive step acting as the generator. This follows the general LogicRealization pattern whose arithmetic object is extracted by the arithmeticOf construction. The logic-natural numbers are the inductive type whose two constructors (identity for the zero-cost element and step for each iteration) form the smallest subset of positive reals closed under multiplication by the generator and containing the identity.
proof idea
The definition is a one-line wrapper that directly applies the orbit equivalence field supplied by the biology realization definition.
why it matters
This definition ensures the biological realization yields the same arithmetic carrier as the logic-forced naturals, closing the extraction step in the universal forcing construction. It supports the general theorem that any realization produces a consistent arithmetic object and thereby embeds generation counts into the T0-T8 chain. No open questions are resolved here, but the equivalence removes a potential mismatch between biological carrier and logic orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.