`syncPeriod`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.RSNativeUnits
domain: Constants
line: 205 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 205.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 202@[simp] noncomputable def gap45 : ℝ := phiRung 45
 203
 204/-- The synchronization period: lcm(8, 45) = 360. -/
 205@[simp] def syncPeriod : ℕ := 360
 206
 207lemma syncPeriod_eq_lcm : syncPeriod = Nat.lcm 8 45 := by native_decide
 208
 209/-! ## K-gate derived displays in RS-native units -/
 210
 211/-- Recognition time display: τ_rec = (2π)/(8 ln φ) · τ₀. -/
 212@[simp] noncomputable def tau_rec : Time :=
 213  Constants.RSUnits.tau_rec_display U
 214
 215/-- Kinematic wavelength display: λ_kin = (2π)/(8 ln φ) · ℓ₀. -/
 216@[simp] noncomputable def lambda_kin : Length :=
 217  Constants.RSUnits.lambda_kin_display U
 218
 219theorem tau_rec_eq_K_gate_ratio :
 220    tau_rec = Constants.RSUnits.K_gate_ratio := by
 221  unfold tau_rec
 222  have hlog : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
 223  simp [Constants.RSUnits.tau_rec_display, Constants.RSUnits.K_gate_ratio, U, tick]
 224  field_simp [hlog]
 225  ring
 226
 227theorem lambda_kin_eq_K_gate_ratio :
 228    lambda_kin = Constants.RSUnits.K_gate_ratio := by
 229  unfold lambda_kin
 230  have hlog : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
 231  simp [Constants.RSUnits.lambda_kin_display, Constants.RSUnits.K_gate_ratio, U, voxel]
 232  field_simp [hlog]
 233  ring
 234
 235/-! ## Planck-Scale Quantities (RS-derived)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.