eleven_check
plain-language theorem explainer
The theorem establishes that the integer 11 differs from both the configuration dimension Dconfig and the eight-tick period eightTick inside the Recognition Science cardinality spectrum. Cross-domain analysts cite it when confirming that 11 enters only via composite routes such as 2 cubed plus D minus two. The proof is a one-line wrapper that applies the decide tactic to the two inequalities.
Claim. The natural number 11 is distinct from the configuration dimension 5 and from the eight-tick cardinality 8.
background
The module shows that cardinalities across the RS stack form a structured spectrum generated from the cube primitives 2 and 3, the configuration dimension 5, and gap45. Dconfig is defined as 5. eightTick is defined as 8, equal to 2 raised to the spatial dimension. The local setting is the C21 claim that RS produces a non-random numerical spectrum in which every listed cardinality admits a decomposition into these primitives.
proof idea
The proof is a term-mode one-liner. It refines the conjunction into two separate goals and applies the decide tactic to each, discharging both inequalities by direct computation on the constants.
why it matters
This check supports the cardinality spectrum by excluding 11 from the base generators, consistent with its description as the less-clean decomposition 2 cubed plus D minus two. It aligns with the framework landmarks T7 eight-tick octave and D equals 3 spatial dimensions. No downstream theorems depend on it, so it functions as an internal consistency witness rather than a lemma for further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.