ten_as_two_halves
plain-language theorem explainer
The natural number equality 10 equals 5 plus 5 supplies the arithmetic split underlying ten-fold combinations across Recognition Science domains. Cross-domain researchers cite it to confirm the 2 times 5 factorization in structures such as fingers, digits, and spinal levels. The proof is a direct decision procedure that verifies the identity in one step.
Claim. $10 = 5 + 5$ in the natural numbers, expressing the factorization of a ten-fold into two five-fold halves.
background
The module C17 asserts that many Recognition Science domains enumerate to 10 via the universal factorization 10 = 2 · 5. Instances include 10 fingers (5 per hand times 2 hands), 10 decimal digits, 10 lumbar plus sacral vertebrae, and 10 d-block elements per period. The doubling is interpreted as pairing a 5-element structure with an orientation or polarity.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to confirm the arithmetic equality.
why it matters
This theorem supplies the core factorization feeding tenFoldCombinationsCert, which aggregates the certifications for fingers, digits, lumbar-sacral vertebrae, and d-block elements. It realizes the C17 structural claim in the Recognition Science framework that ten equals two times five. The result anchors cross-domain enumeration without reference to the J-cost or phi-ladder from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.