LumbarSacralVert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove cardinality 10; that step occurs in the downstream lumSac_is_10 theorem.
- Does not address cervical, thoracic, or coccygeal vertebrae.
- Does not derive any dynamical or physical properties from the enumeration.
- Does not invoke J-cost, defectDist, or the phi-ladder mass formula.
formal statement (Lean)
40inductive LumbarSacralVert where
41 | l1 | l2 | l3 | l4 | l5 | s1 | s2 | s3 | s4 | s5
42 deriving DecidableEq, Repr, BEq, Fintype
43