`alphaLock_lt_one`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants on GitHub at line 234.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 231  have : 1 / phi < 1 := (div_lt_one phi_pos).mpr hphi
 232  linarith
 233
 234lemma alphaLock_lt_one : alphaLock < 1 := by
 235  have hpos : 0 < phi := phi_pos
 236  unfold alphaLock
 237  have : 1 / phi > 0 := one_div_pos.mpr hpos
 238  linarith
 239
 240/-- Canonical locked C_lag constant: C_lock = φ^{−5}. -/
 241@[simp] noncomputable def cLagLock : ℝ := phi ^ (-(5 : ℝ))
 242
 243lemma cLagLock_pos : 0 < cLagLock := by
 244  have hphi : 0 < phi := phi_pos
 245  unfold cLagLock
 246  exact Real.rpow_pos_of_pos hphi (-(5 : ℝ))
 247
 248/-- The elementary ledger bit cost J_bit = ln φ. -/
 249noncomputable def J_bit : ℝ := Real.log phi
 250
 251/-- Coherence energy in RS units (dimensionless).
 252    By Phase 2 derivation, E_coh = C_lock = φ⁻⁵. -/
 253noncomputable def E_coh : ℝ := cLagLock
 254
 255lemma E_coh_pos : 0 < E_coh := cLagLock_pos
 256
 257/-! ### RS-native fundamental units (parameter-free)
 258
 259The **core theory** is expressed in RS-native units:
 260
 261- `tau0 = 1` tick (time quantum)
 262- `ell0 = 1` voxel (length quantum)
 263- `c = 1` voxel/tick
 264

papers checked against this theorem

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