biologyCost_symm
plain-language theorem explainer
Symmetry of the generation-comparison cost in the biological realization of the forcing chain. Researchers modeling biology via Recognition Science would cite this to confirm the cost metric is undirected. The proof proceeds by case analysis on equality of the two generations, followed by substitution or symmetric inequality and simplification using the cost definition.
Claim. For generations $a$ and $b$, the cost function defined by $c(a,b) := 0$ if $a = b$ and $1$ otherwise satisfies $c(a,b) = c(b,a)$.
background
In the BiologyRealization module the carrier is the generation count, realized as the natural-number type Generation. The biologyCost function returns zero on identical generations and one otherwise, providing the comparison metric for the reproductive step as generator. This lightweight model sits inside the universal forcing framework and imports the EthicsRealization context while depending on the Generation type from SpectralEmergence (Fin 3) and the inductive Generation types appearing in CKM, ThreeGenerations, and RSLedger.
proof idea
The tactic proof opens with by_cases on a = b. The equal case substitutes and simplifies both sides to zero via the biologyCost definition. The unequal case first derives the symmetric inequality b ≠ a, then simplifies both biologyCost applications to one.
why it matters
The result is invoked inside the biologyRealization definition that builds a LogicRealization with Carrier := Generation and Cost := biologyCost. It guarantees the cost is symmetric, aligning with the undirected comparisons required by the Recognition Composition Law and the T0–T8 forcing chain. The lemma closes a basic symmetry obligation for the biological carrier before further realization steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.