rsKeyIdentityCount
plain-language theorem explainer
The definition assigns the natural number five to the count of canonical Recognition Science number-theoretic identities. Researchers building certificates for the complete set of these identities reference the constant when verifying the catalogue. The declaration is a direct constant assignment requiring no lemmas or computation.
Claim. Let $k$ be the count of the five key number-theoretic identities derived from Recognition Science. Then $k=5$.
background
The module Number Theory from RS catalogues five key identities from the Recognition Science framework: the golden ratio equals itself, its square equals one plus itself, its fifth power equals five times itself plus three, its eighth power exceeds forty-six, and its forty-fourth power exceeds ten to the eight. These identities arise from the phi-ladder relations and the gap45 construction at three spatial dimensions. The local setting states that all five have already been proved in prior modules with zero sorry or axioms, and the definition simply records their total count.
proof idea
This is a direct constant definition assigning the value five. No lemmas are applied and no tactics are used; the declaration serves as a reference value for downstream structures and theorems.
why it matters
The definition is referenced inside the NumberTheoryCert structure, which bundles the five identities together with the count, and inside the theorem rsi_count_five that proves the count equals five by reflexivity. It completes the explicit catalogue step described in the module documentation, supporting the Recognition Science derivation of number theory from the phi-ladder and gap45 without introducing new open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.