NumberTheoryCert
plain-language theorem explainer
NumberTheoryCert bundles five canonical RS identities into one structure for reference in derivations on the phi-ladder. Researchers working on gap45 relations or baryon rung bounds would cite it when needing a single certificate for the phi-squared, phi-fifth, phi-eighth, dimensional-gap, and count identities. The declaration is a pure structure definition whose fields directly encode the relations proved in sibling lemmas.
Claim. A structure $C$ certifying the identities $C.phi_{sq} : phi^2 = phi + 1$, $C.phi_5 : phi^5 = 5 phi + 3$, $C.phi_8 : phi^8 = 21 phi + 13$, $C.gap_{45,D} : 3^2 (3 + 2) = 45$, and $C.five_{identities} :$ the count of key RS number-theoretic identities equals 5.
background
Recognition Science extracts number theory from the J-cost functional equation whose self-similar fixed point is the golden ratio phi. The module catalogues five identities: the algebraic relation phi squared equals phi plus one, the Fibonacci relation phi to the fifth equals five phi plus three, phi to the eighth equals twenty-one phi plus thirteen, the spatial-dimension identity nine times five equals forty-five at D equals three, and the statement that exactly five such identities exist. These rest on the phi-ladder and gap45 definitions introduced in upstream modules. The single upstream dependency rsKeyIdentityCount is the constant definition equal to five.
proof idea
Direct structure definition with no proof body. The five fields are typed as the respective equalities; no tactics or reductions are applied inside this declaration.
why it matters
The structure supplies the single object instantiated by the downstream numberTheoryCert definition, which in turn feeds mass-formula and forcing-chain derivations. It directly records the five identities listed in the module documentation, closing the gap45 relation at D equals three and supporting the T6 phi fixed-point and T8 dimension steps of the unified forcing chain. No open scaffolding remains inside the declaration itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.