Gap45Region
plain-language theorem explainer
A Gap-45 region is the structure whose synchronization period equals 360. Lattice theorists analyzing near-degenerate attractors cite it when the eight-tick octave meets the 45-rung phi-ladder at their least common multiple. The definition is supplied directly by assignment of the period together with a reflexivity proof of the equality.
Claim. A Gap-45 region is the structure whose synchronization period $s$ satisfies $s=360$, where $360= lcm(8,45)$, $8$ is the octave length from the eight-tick cadence, and $45$ is the rung count on the phi-ladder.
background
The module introduces the Gap-45 phenomenon as the synchronization period of the recognition lattice. The 8-tick cadence arises from the octave (T7: $2^3=8$) while the 45-rung count comes from the phi-ladder; their least common multiple is 360. At this boundary the J-cost landscape becomes nearly flat, with energy differences smaller than phi to the minus 45, forming a degenerate basin. Upstream, DimensionForcing defines sync_period as Nat.lcm eight_tick gap_45, Constants supplies octave as 8 times the tick, and MusicalScale records the octave ratio as 2.
proof idea
The structure is introduced by direct field assignment of sync_period to 360. The accompanying equality is discharged by the reflexivity tactic rfl.
why it matters
This definition supplies the concrete 360-tick object required by the Gap-45 construction in the foundation module. It directly implements the lcm(8,45) step that produces the flat J-cost landscape whose degenerate basin is invoked for the free-will mechanism. The construction sits inside the T7 eight-tick octave and the phi-ladder rung counting of the forcing chain; downstream siblings such as gap45_from_lcm and gap45_creates_flat_landscape build on the same period.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.