ten_is_2_D
The equality 10 equals twice the configuration dimension holds as a basic arithmetic fact in the Recognition Science cardinality spectrum. Cross-domain analysts would cite this witness when decomposing spectrum entries into primitives such as 2 and 5. The proof reduces to a direct numerical decision on natural numbers.
claim$10 = 2 D$ where the configuration dimension $D$ is defined to be 5.
background
In the CrossDomain.CardinalitySpectrum module the configuration dimension is fixed at 5. This module assembles witnesses that every entry in the RS spectrum, including 10, arises from multiplication or combination of the small generators 2, 3 and the config dimension 5. The local setting states that RS produces a structured numerical spectrum rather than arbitrary values, with each member admitting a decomposition into these primitives.
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm the arithmetic equality between 10 and twice the configuration dimension.
why it matters in Recognition Science
This theorem supplies a concrete witness for the entry 10 in the RS cardinality spectrum presented as part of the structured set reachable from RS primitives. It supports the module claim that the spectrum is generated by operations on 2, 3 and the config dimension 5. No downstream theorems depend on it and no open questions are addressed.
scope and limits
- Does not derive the configuration dimension from deeper axioms.
- Does not address other spectrum entries or their decompositions.
- Does not connect the cardinalities to physical interpretations.
formal statement (Lean)
58theorem ten_is_2_D : (10 : ℕ) = 2 * Dconfig := by decide
proof body
Term-mode proof.
59
60/-- 12 = 3·4 = D · 2² (cube edges). -/