Gap45 Group View

The coprime intersection

In group theory, the order of an element is the smallest positive power that returns it to the identity. A standard fact: if an element's order divides two numbers, it also divides their greatest common divisor. The gap45 group view applies this to the numbers 8 and 45, which share no common factor besides 1.

The lemma states: if an element g in any group satisfies g^8 = 1 and g^45 = 1, then g must equal the identity element. The proof is short. From each power condition, the order of g divides 8 and divides 45. Therefore the order divides their gcd, which is 1. An element whose order divides 1 has order exactly 1, meaning it is the identity.

This is not a deep theorem but a useful structural tool. It shows that two coprime power conditions cannot coexist for a nontrivial element. The result holds for every group, finite or infinite, abelian or not, because it relies only on the definition of order and divisibility.

In Recognition Science, this lemma appears in the framework's machine-checked library of formal theorems as a building block. The framework uses it where elements are constrained by multiple power conditions, and the coprime pair 8 and 45 collapses the possibilities to a single outcome. The practical payoff: when a group element satisfies both conditions, no further analysis is needed, it is the identity.

/-- 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 module does not define the numbers 8 or 45 as fundamental constants. The lemma does not require the group to be finite or abelian. No claim is made about how this lemma connects to the broader forcing chain.

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: