fortyfive_sub_eight_eq_thirtyseven
plain-language theorem explainer
The equality 45 minus 8 equals 37 is recorded as a stable arithmetic anchor for the RS beat numerator. Researchers citing the phi-ladder or eight-tick octave constants reference it to avoid repeating the subtraction in bridge lemmas. The proof reduces to a single native_decide tactic that evaluates the natural-number subtraction directly.
Claim. $45 - 8 = 37$
background
The module gathers small decidable arithmetic facts about integers such as 8, 45, 360, and 840 that recur across the repo. These serve as fixed anchors so later lemmas remain readable without re-proving the same subtractions or factorizations. The upstream CirclePhaseLift.and supplies an explicit log-derivative bound M on a disk, though the present declaration uses only direct computation.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the subtraction on natural numbers and confirm the result.
why it matters
This records the RS beat numerator as the difference 45 - 8 = 37, filling the module's role of stable anchors for prime facts and factorizations. It supports the eight-tick octave (period 2^3) in the forcing chain by keeping arithmetic explicit for constants that appear in the phi-ladder. No open questions remain; the result is fully proved by computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.