_biology_ok
plain-language theorem explainer
The definition asserts that the Peano carrier extracted from the arithmetic of the strict biological realization matches the natural numbers forced directly by the law of logic. Researchers auditing domain-specific realizations within the universal forcing framework would cite it to confirm arithmetic consistency across biology. The construction is a direct one-line wrapper that invokes the orbit equivalence supplied by the lightweight conversion of the realization.
Claim. Let $R$ be the strict realization of biology with reproduction as the composition operation. The carrier of the Peano structure in the arithmetic derived from $R$ is equivalent to the natural numbers induced by the law of logic: $((arith(R)).peano.carrier) ≃ LogicNat$.
background
The AxiomAudit module supplies surface verification for strict realizations of the universal forcing. A StrictLogicRealization is a structure consisting of a carrier type, a cost type equipped with a zero instance, a comparison map, and a composition operation. The strict biological realization instantiates this structure using lineage states as carrier and reproduction as composition, treating reproduction as the generator of the orbit.
proof idea
The definition is a one-line wrapper that applies the orbit equivalence from the lightweight realization of the strict biological realization.
why it matters
This equivalence confirms that the biological realization obeys the general property that every strict realization yields arithmetic canonically equivalent to the logic natural numbers. It contributes to the audit surface for the strict universal forcing completion in the foundation layer, aligning with the forcing chain in which arithmetic emerges from the law of logic. No downstream uses are recorded, indicating its primary role in verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.