`syncPeriod_eq_lcm`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 207.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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)
 236
 237In RS, the Planck scale emerges from the gate identities, not as a postulate.

papers checked against this theorem

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