trivial_intersection_nsmul
plain-language theorem explainer
In an additive group, an element a satisfying 8a=0 and 45a=0 must be zero. Researchers analyzing periodic structures in Recognition Science Gap45 would cite this to enforce triviality under combined 8-tick and 45-step conditions from the phi-ladder. The tactic proof extracts the additive order via divisibility lemmas, reduces it through the gcd, and concludes a=0 from order one.
Claim. Let $(A,+)$ be an additive group and $a$ an element of $A$. If $8a=0$ and $45a=0$, then $a=0$.
background
The Gap45.AddGroupView module supplies an additive-group perspective on intersection properties arising from the Recognition Science forcing chain. Upstream definitions set A to the active edge count per fundamental tick (value 1), appearing in IntegrationGap as the phi-power balance identity at D=3, in Masses.Anchor as the coherence energy unit, and in Modal.Actualization as the actualization operator mapping configurations to their J-minimizers. The lemma operates inside Mathlib's AddGroup structure, where nsmul denotes repeated addition and addOrderOf tracks the minimal positive integer n with na=0.
proof idea
The tactic proof applies addOrderOf_dvd_iff_nsmul_eq_zero twice to obtain that the additive order of a divides 8 and divides 45. It then invokes Nat.dvd_gcd to conclude the order divides 1. Nat.dvd_one reduces this to order exactly 1, after which addOrderOf_eq_one_iff yields a=0.
why it matters
This lemma supplies the trivial-intersection step needed for Gap45 analyses that combine the eight-tick octave (T7) with the 45-step phi-balance identity. It supports the D=3 spatial dimension claim by eliminating nontrivial elements that could satisfy both periodicity conditions simultaneously. No downstream theorems are recorded, so the result functions as a local closure for additive representations of the RCL and phi-ladder relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.