LumbarSacralVert
plain-language theorem explainer
LumbarSacralVert is an inductive type with ten constructors enumerating the five lumbar and five sacral vertebrae. Cross-domain researchers cite it as one concrete instance of the 2×5 factorization that appears across Recognition Science structures. The declaration is a direct inductive definition equipped with DecidableEq, Repr, BEq, and Fintype derivations.
Claim. Let $V$ be the inductive type whose constructors are $l_1,l_2,l_3,l_4,l_5,s_1,s_2,s_3,s_4,s_5$, equipped with decidable equality, a representation function, boolean equality, and finite-type structure.
background
The CrossDomain.TenFoldCombinations module asserts that multiple Recognition Science domains enumerate to cardinality 10, factorizing universally as 10 = 2 × 5. LumbarSacralVert supplies the lower axial example: five lumbar vertebrae paired with five sacral vertebrae. The sibling predicate HasTenFold asserts that a type has exactly ten inhabitants; downstream theorems apply it directly to this inductive type.
proof idea
The declaration is an inductive definition that introduces the ten constructors explicitly. No lemmas or tactics are invoked; the type is constructed to match the required cardinality for the ten-fold property.
why it matters
LumbarSacralVert supplies the lumSac_10 field inside TenFoldCombinationsCert, which aggregates HasTenFold instances for Finger, DecimalDigit, LumbarSacralVert, and DBlockElement together with the equation 10 = 2 * 5. It realizes the spinal-level case listed in the module documentation for the C17 ten-fold claim, reinforcing the recurring 2·5 pattern that sits alongside the eight-tick octave and phi-ladder constructions in the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.