lineageCost_symm
plain-language theorem explainer
Symmetry of the discrete cost on lineage states, each a pair of natural-number lineage label and generation depth, holds for every pair. Researchers constructing discrete generational models as costed logic realizations cite it to confirm the compare operation is undirected. The proof uses case analysis on state equality, followed by substitution and simplification against the cost definition.
Claim. For all states $a$ and $b$, each consisting of a lineage label and generation depth, the cost $c(a,b)$ equals $c(b,a)$, where $c(x,y)$ returns 0 if $x=y$ and 1 otherwise.
background
A lineage state pairs a natural-number lineage label with a generation depth; the label prevents reduction to a bare natural-number type, so arithmetic must be generated by repeated reproductive steps. The cost between two states is defined to return 0 on equality and 1 on inequality. This pair supplies the carrier and compare operation for the strict biological realization of logic.
proof idea
Case analysis on whether the two states coincide. On equality, substitute and simplify directly with the cost definition. On inequality, derive the symmetric inequality and simplify the cost definition under both conditions to obtain equality of the resulting 1 values.
why it matters
The result feeds strictBiologyRealization, which packages lineage states, the cost, and reproduction into a StrictLogicRealization. It supplies the symmetry required for the compare operation inside the Universal Forcing chain, ensuring the biological carrier satisfies the basic algebraic properties demanded by the forcing construction without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.