`alphaLock_lt_one`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants on GitHub at line 234.

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

 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.