sub_mul_add_eq_sq_sub_one
plain-language theorem explainer
For every natural number b at least 1, truncated subtraction satisfies (b-1)(b+1)=b^{2}-1 in ℕ. Period-factor extraction cites this to turn a square congruence into a product of consecutive offsets. The proof lifts b=1+k, cancels, rings the sum identity, then applies Nat.eq_sub_of_add_eq and pow_two.
Claim. For every natural number $b\ge 1$, the identity $(b-1)(b+1)=b^2-1$ holds in $\mathbb{N}$ under truncated subtraction.
background
Lean’s natural-number subtraction is truncated: $b-1=0$ when $b=0$. The hypothesis $b\ge 1$ restores the classical difference-of-squares factorization inside $\mathbb{N}$.
The surrounding PeriodFactor module extracts proper divisors from even periods. Downstream, if $n\mid b^2-1$ while $n$ divides neither $b-1$ nor $b+1$, then $\gcd(b-1,n)$ is a nontrivial proper factor of $n$. That argument needs $(b-1)(b+1)=b^2-1$ so that a divisor of the square difference is a divisor of the product of the two offsets.
Local setting is Foundation primitive-recognition calculus: discrete period structure (including the eight-tick octave) motivates asking when a period forces a nontrivial factor of a modulus.
proof idea
From $1\le b$, obtain $b=1+k$ via Nat.exists_eq_add_of_le. After Nat.add_sub_cancel_left, the goal reduces to showing $(b-1)(b+1)+1=b\cdot b$. The substituted expression is handled by ring. Then Nat.eq_sub_of_add_eq rewrites the product as $b\cdot b-1$, and pow_two turns the right-hand side into $b^2-1$. Pure Nat arithmetic; no external RS lemmas.
why it matters
Feeds even_period_yields_factor, which states: if $2\le n$, $1\le b$, $n\mid b^2-1$, yet $n$ divides neither $b-1$ nor $b+1$, then $1<\gcd(b-1,n)<n$. That theorem is the algebraic engine behind nontrivialFactorization_of_even_period_gap and the PeriodFactorCertificate in the same module.
In the Recognition forcing chain, period factorization supports the discrete spectrum tied to the eight-tick octave (T7). The identity is elementary, but without a truncated-subtraction proof the modular product step would not typecheck in $\mathbb{N}$. It closes a small scaffolding gap so the factor-extraction certificate can be stated without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.