eleven_check
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assert any specific decomposition formula for 11.
- Does not claim that 11 is absent from the overall spectrum.
- Does not address whether 11 satisfies the Recognition Composition Law or other RS relations.
- Does not extend to interpretations outside natural numbers.
formal statement (Lean)
99theorem eleven_check : (11 : ℕ) ≠ Dconfig ∧ (11 : ℕ) ≠ eightTick := by
proof body
Term-mode proof.
100 refine ⟨?_, ?_⟩ <;> decide
101
102/-- 13 = F(7), a Fibonacci number (cleanly interpretable via φ-ladder). -/