sync_exceeds_both
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute or prove the explicit lcm value beyond the supplied inequality.
- Does not address J-cost or local excitations at misaligned voxels.
- Does not connect to mass formulas or Berry creation thresholds.
- Does not quantify the density of misalignment voxels.
formal statement (Lean)
50theorem sync_exceeds_both :
51 gap45.sync_period > gap45.recognition_period ∧
52 gap45.sync_period > gap45.phase_period := by
proof body
Term-mode proof.
53 constructor <;> simp [gap45, Gap45Frustration.sync_period,
54 Gap45Frustration.recognition_period, Gap45Frustration.phase_period,
55 syncPeriod_3]
56 all_goals norm_num
57
58/-! ## The Perpetual Complexity Theorem -/
59
60/-- At every 360-tick boundary, there exist voxels where the recognition
61 and phase cadences are misaligned. These voxels have positive local
62 J-cost (they are not at x=1) and constitute structured excitations. -/