IndisputableMonolith.Gap45.AddGroupView
The Gap45.AddGroupView module states the additive group version of the trivial intersection for Gap45. If an element a satisfies 8a = 0 and 45a = 0 in an additive group, then a = 0 because the order divides gcd(8,45) = 1. This supplies the additive perspective needed for the Recognition Science forcing chain. The module imports Mathlib and relies on standard order and gcd facts.
claimLet $G$ be an additive group. If $8a = 0_G$ and $45a = 0_G$, then $a = 0_G$.
background
The module sits in the Gap45 domain and imports Mathlib to access additive group operations. It formalizes scalar multiplication n • a as the n-fold sum of a with itself. The doc comment supplies the core claim: the additive order of a divides both 8 and 45, hence divides 1. This setting complements the eight-tick octave structure from the upstream forcing chain.
proof idea
This is a module containing the additive statement with no proof body lines shown. The argument is the direct consequence that the order divides gcd(8,45)=1, forcing a=0. It uses the sibling trivial_intersection_nsmul for the underlying order property.
why it matters in Recognition Science
The module supplies the additive view that feeds the Gap45 construction and the broader monolith theorems on uniqueness. It fills the additive half of the intersection result that supports T7 octave periodicity and the fixed-point properties in the Recognition Science chain.