tenFoldCombinationsCert
plain-language theorem explainer
The declaration assembles a certificate verifying that multiple structures in Recognition Science satisfy the ten-fold property through the factorization 10 = 2 × 5. A researcher studying cross-domain enumerations would cite it to link examples such as the ten fingers, decimal digits, lumbar-sacral vertebrae, and d-block elements. The construction is a direct record definition that references the individual HasTenFold proofs and the arithmetic identities.
Claim. The structure asserts that Finger, DecimalDigit, LumbarSacralVert, and DBlockElement each satisfy the ten-fold predicate, together with the identities $10 = 2 × 5$ and $10 = 5 + 5$, and that the Cartesian product of any two ten-fold sets has cardinality 100.
background
TenFoldCombinationsCert packages instances of the HasTenFold predicate for four concrete types along with the numerical identities 10 = 2·5 and 10 = 5+5 and a product-closure rule. HasTenFold A holds when the finite type A has cardinality exactly 10. The module treats this factorization as the universal pattern behind ten-fold enumerations in Recognition Science domains.
proof idea
The definition builds the record by direct field assignment: finger_is_10 supplies the Finger instance, digit_is_10 the DecimalDigit instance, lumSac_is_10 the LumbarSacralVert instance, dBlock_is_10 the DBlockElement instance, ten_eq_two_D the factoring identity, ten_as_two_halves the sum identity, and a lambda that invokes tenfold_squared for the product rule.
why it matters
This definition realizes the C17 claim that ten-fold combinations arise uniformly as 2·5 or 5+5 pairings across domains. It supplies the concrete certificate for the structural pattern 10 = 2D that appears in cancer hallmarks, sense types, spinal segments, and periodic-table blocks. No downstream theorems yet invoke the certificate, leaving open its integration into larger cross-domain results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.