sync_exceeds_both
plain-language theorem explainer
The theorem states that the synchronization period of 360 ticks exceeds both the 8-tick recognition period and the 45-tick phase period. Cosmologists working on perpetual complexity in Recognition Science cite it to establish persistent cadence misalignment. The proof is a term-mode constructor that simplifies the Gap45Frustration fields and normalizes the resulting numerical comparisons.
Claim. Let $P_r = 8$, $P_p = 45$, and $P_s = 360$. Then $P_s > P_r$ and $P_s > P_p$.
background
The Gap45Frustration structure in this module sets recognition_period to 8 ticks and phase_period to 45 ticks with their coprimality, defining sync_period as their lcm. The upstream sync_period definition from DimensionForcing confirms this lcm equals 360, while the eight-tick phase definition supplies the underlying cadence. The module doc states that this combines with positive vacuum energy from passive modes to guarantee local complexity at every epoch, referencing Dark_Energy_Mode_Counting.tex §10 Theorem 10.1.
proof idea
The term proof applies constructor to split the conjunction, then simp unfolds Gap45Frustration.sync_period, recognition_period, phase_period together with syncPeriod_3, and norm_num discharges the concrete inequalities 360 > 8 and 360 > 45.
why it matters
This inequality is a required step inside the Perpetual Complexity Theorem, confirming that the lcm period never collapses to either component cadence. It directly supports the module's no_heat_death claim and the PerpetualComplexityCert by ensuring misalignment voxels exist at every 360-tick boundary. The result rests on the eight-tick octave (T7) and gap-45 coprimality, closing one link in the chain that prevents global synchronization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.