biology_admissible
plain-language theorem explainer
The definition supplies an AdmissibleRealization instance for the strict biology realization by confirming decidable lineage costs, associative reproduction, and idempotence of the zero lineage state. Researchers citing the quantified universal forcing theorem reference it to include the biology domain among the admissible realizations. The construction is a direct refinement of the three structure fields using decidable equality, the reproduction associativity lemma, and reflexivity.
Claim. Let $R$ be the strict biology realization with carrier LineageState, cost function returning 0 on equality and 1 otherwise, and composition given by reproduction. Then $R$ admits an admissible realization: its cost predicate is decidable, reproduction is associative, and reproduction of the zero lineage state with itself yields the zero lineage state.
background
A StrictLogicRealization equips a carrier with a cost function and composition operation. For biology the carrier is LineageState (lineage identifier paired with generation depth), the cost is lineageCost (0 if states match, 1 otherwise), and composition is reproduce (adds generation depths while copying the lineage). The AdmissibleRealization structure augments any such realization with three properties: decidability of zero-cost equality, associativity of composition, and a nontrivial identity condition on the unit (lineageZero). This definition draws on the upstream reproduce_assoc theorem, which proves associativity by unfolding reproduce and applying Nat.add_assoc.
proof idea
The definition refines the three fields of AdmissibleRealization. The cost_decidable field is witnessed by decidable equality on the output of lineageCost. The compose_assoc field is supplied directly by the reproduce_assoc theorem. The compose_one_or_step field is discharged by the left disjunct, showing reproduce(lineageZero, lineageZero) equals lineageZero by reflexivity.
why it matters
This definition populates the biology_adm field inside admissibleClassCert_holds, which assembles the witnesses needed for quantified_universal_forcing. It also contributes to four_canonical_domains_admissible, which records nonempty admissible realizations for the four canonical domains. In the Recognition Science setting it ensures the biology domain participates in the canonical equivalence of forced arithmetic surfaces across admissible realizations rather than arbitrary strict realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.