eight_eq_two_pow_three
plain-language theorem explainer
The natural-number equality 8 equals 2 to the power 3 fixes a basic power-of-two identity. Recognition Science workers cite it when anchoring the eight-tick octave period without recomputing the arithmetic each time. The proof is a one-line wrapper that invokes native_decide on the decidable equality.
Claim. $8 = 2^3$ holds in the natural numbers.
background
The RSConstants module gathers small decidable arithmetic facts about integers such as 8, 45, 360 and 840. These facts serve as stable anchors that keep later bridge lemmas readable and avoid re-proving the same arithmetic in many places. The module imports Mathlib together with the Basic and Factorization files from the same primes subdirectory.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to discharge the decidable equality.
why it matters
This equality anchors the eight-tick octave (period 2^3) at forcing-chain step T7. It supplies a concrete numerical fact that stabilizes expressions involving powers of two in later number-theoretic bridges inside the Recognition Science framework. No downstream theorems are recorded, yet the fact supports the module's collection of prime markers and factorizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.