TenFoldCombinationsCert
plain-language theorem explainer
TenFoldCombinationsCert packages four concrete 10-element types from distinct domains together with the arithmetic identities 10 = 2·5 and 10 = 5 + 5, plus the general fact that the cartesian product of any two 10-fold finite types has cardinality 100. A cross-domain researcher would cite it when unifying enumerations such as fingers, digits, spinal segments and d-block elements under the Recognition Science factorization 10 = 2D. The structure is a plain record definition with no proof obligations beyond the inductive constructions of the four
Claim. Let $F$, $D$, $L$, $B$ be the finite types of fingers, decimal digits, lumbar-sacral vertebrae, and first-period d-block elements. Then $|F| = |D| = |L| = |B| = 10$, $10 = 2 × 5$, $10 = 5 + 5$, and for any finite types $A$, $B$ with $|A| = |B| = 10$, $|A × B| = 100$.
background
HasTenFold T is the proposition that a finite type T satisfies Fintype.card T = 10, equivalently the factorization 2·5. The four types are introduced by induction: Finger lists ten left- and right-hand digits, DecimalDigit the symbols 0-9, LumbarSacralVert the five lumbar plus five sacral vertebrae, and DBlockElement the ten elements scandium through zinc. Module C17 presents these as instances of the universal 10 = 2D splitting that recurs in cancer hallmarks, sense modalities, commandments, and periodic-table blocks. Upstream results supply only the Fintype.card definition and the four inductive enumerations; the IntegrationGap.A edge count is imported but unused here.
proof idea
The declaration is a direct structure definition whose fields are propositions. Each HasTenFold field is witnessed by the corresponding sibling lemma (finger_is_10, digit_is_10, lumSac_is_10, dBlock_is_10) that evaluates Fintype.card of the inductive type. The two arithmetic identities are supplied by ten_eq_two_D and ten_as_halves. The squared_100 field is the universal statement whose proof is deferred to the downstream cert construction.
why it matters
The structure supplies the concrete data for the C17 claim that ten-fold enumerations recur across domains via the factorization 10 = 2·5. It is instantiated by the downstream definition tenFoldCombinationsCert, which populates the record using the per-type lemmas and the arithmetic facts. In the Recognition framework it supports the eight-tick octave by exhibiting the 2·5 splitting that aligns with the doubling in the phi-ladder. No open scaffolding remains; the module reports zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.