TenFoldCombinationsCert
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
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the 10-fold property from the Recognition Composition Law.
- Does not connect these cardinalities to the phi-ladder mass formula.
- Does not address whether other domains admit 10-fold structure.
- Does not prove uniqueness of the 2·5 factorization.
formal statement (Lean)
81structure TenFoldCombinationsCert where
82 finger_10 : HasTenFold Finger
83 digit_10 : HasTenFold DecimalDigit
84 lumSac_10 : HasTenFold LumbarSacralVert
85 dBlock_10 : HasTenFold DBlockElement
86 ten_factoring : (10 : ℕ) = 2 * 5
87 ten_as_halves : (10 : ℕ) = 5 + 5
88 squared_100 : ∀ (A B : Type) [Fintype A] [Fintype B],
89 HasTenFold A → HasTenFold B → Fintype.card (A × B) = 100
90