Gap45 Group View Trivial Intersection Pow

The coprime power lemma

In group theory, the order of an element is the smallest positive number of times it must be combined with itself to obtain the identity. A basic fact connects orders to powers: if an element raised to some power equals the identity, then the element's order divides that power. The lemma trivial_intersection_pow applies this to the numbers 8 and 45. Since these two numbers share no common factor greater than 1, their greatest common divisor is 1. Therefore, if an element's 8th power and its 45th power are both the identity, its order must divide 1, which forces the order to be 1, meaning the element itself is the identity.

The proof is a short chain of standard group-theoretic facts. From the hypothesis that g^8 = 1, the lemma derives that the order of g divides 8. From g^45 = 1, it derives that the order divides 45. Since the order divides both numbers, it divides their greatest common divisor, which is 1. The only positive integer dividing 1 is 1 itself, so the order is 1, and an element of order 1 is the identity. This is a fully formal proof checked by a machine, with no hidden assumptions beyond the standard axioms of logic and set theory.

In Recognition Science, this lemma appears as part of a larger structural analysis of the group of order 45. The framework uses machine-checked libraries of formal theorems to build its results, and this lemma is one small brick in that construction. The lemma itself is not specific to recognition or to the framework's distinctive concepts; it is a general fact about groups that holds in any group, regardless of what the group elements represent. Its role in the framework is to establish a clean intersection property: the subgroups generated by elements of 8-power and 45-power type meet only at the identity.

What the lemma does not claim is just as important. It does not say anything about the structure of the group of order 45 beyond this one intersection fact. It does not identify which group of order 45 is being studied, nor does it assert that such a group exists. It does not involve the golden ratio, the eight-tick cycle, or any other Recognition Science constant. The lemma is a standalone group-theoretic result, proved in full generality for any group and any element satisfying the two power conditions.

The practical consequence is a clean separation: when working inside the framework, this lemma gives a quick way to recognize that certain elements are trivial, without needing to know anything else about the group. It is a tool, not a conclusion about the physical world. A reader who wants to understand what the framework proves about groups of order 45 will need additional lemmas; this one merely clears the ground.

/-- If an element `g` has both 8‑power and 45‑power equal to identity in a group,
its order divides `gcd(8,45)=1`, hence `g = 1`. -/
lemma trivial_intersection_pow {G : Type*} [Group G] {g : G}
  (h8 : g ^ 8 = 1) (h45 : g ^ 45 = 1) : g = 1 := by
  have h8d : orderOf g ∣ 8 := orderOf_dvd_of_pow_eq_one h8
  have h45d : orderOf g ∣ 45 := orderOf_dvd_of_pow_eq_one h45
  have hgcd : orderOf g ∣ Nat.gcd 8 45 := Nat.dvd_gcd h8d h45d
  have hone : orderOf g ∣ 1 := by simpa using hgcd
  have h1 : orderOf g = 1 := Nat.dvd_one.mp hone
  exact (orderOf_eq_one_iff.mp h1)

What this page does not claim

This lemma does not describe the structure of any specific group of order 45. The lemma does not involve Recognition Science constants such as the golden ratio or the eight-tick cycle. The proof does not rely on any Recognition Science-specific axioms.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gap45/GroupView.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: