trivial_intersection_pow
plain-language theorem explainer
In any group, an element g satisfying both g^8 = 1 and g^45 = 1 must be the identity. Modelers of periodic symmetries in Recognition Science or group theorists handling finite-order constraints would cite this when proving triviality of intersections under coprime exponents. The proof reduces the claim to the order of g dividing gcd(8,45)=1 via standard divisibility lemmas on orders.
Claim. Let $G$ be a group with identity $e$. For $g$ in $G$, if $g^8 = e$ and $g^{45} = e$, then $g = e$.
background
The lemma sits in the Gap45.GroupView module, which applies group theory to structures with periods 8 and 45. Here the order of an element g is the least positive integer k such that g^k equals the identity; the key fact used is that g^k = e implies this order divides k. The module imports Mathlib for these primitives and sits inside the larger IndisputableMonolith development that also defines constants such as the gravitational G in RS-native units.
proof idea
Tactic-mode proof. Apply orderOf_dvd_of_pow_eq_one to the two hypotheses to obtain that the order divides 8 and divides 45. Combine via Nat.dvd_gcd to reach divisibility by gcd(8,45)=1. Use simpa to reduce to divisibility by 1, then Nat.dvd_one.mp to conclude the order equals 1. Finish with orderOf_eq_one_iff.mp to recover g=1.
why it matters
The result supplies a trivial-intersection fact inside the Gap45 analysis, consistent with the eight-tick octave (T7) of the forcing chain. It helps close group-theoretic constraints that arise when periods must be compatible with the phi-ladder and D=3 spatial structure. With no downstream uses recorded, it functions as an internal helper rather than a top-level theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.