lumSac_is_10
plain-language theorem explainer
The theorem establishes that the inductive type of five lumbar and five sacral vertebral levels has cardinality exactly 10. Researchers building cross-domain enumerations in Recognition Science cite the result when certifying that multiple systems share the factorization 10 = 2 × 5. The proof is a one-line wrapper that unfolds the cardinality predicate and lets the decide tactic confirm the count via the derived finite-type instance.
Claim. The finite type consisting of the five lumbar levels l1–l5 together with the five sacral levels s1–s5 has cardinality 10, i.e., its size equals 2 · 5.
background
The module introduces the predicate that a finite type T satisfies the ten-fold condition precisely when its cardinality equals 10, which encodes the universal factorization 10 = 2 · 5 obtained by pairing a five-element structure with a binary orientation or alternation. The inductive type enumerates the ten lower axial spinal levels as five lumbar followed by five sacral, matching the module documentation’s list of instances that includes fingers, decimal digits, and d-block elements. This local setting sits inside the C17 structural claim that many RS domains realize the same enumerative pattern.
proof idea
The proof is a one-line wrapper. It unfolds the cardinality predicate to expose the equality Fintype.card T = 10, then applies the decide tactic, which succeeds because the inductive type derives both Fintype and DecidableEq.
why it matters
The declaration supplies the lumSac_10 field required by the tenFoldCombinationsCert definition that assembles the complete certificate for the ten-fold claim. It directly instantiates the module’s C17 enumerative statement for the axial skeleton without invoking the forcing chain, J-uniqueness, or phi-ladder. The result closes one concrete instance in the cross-domain wave 63 program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.