pith. machine review for the scientific record. sign in
def

alphaLock

definition
show as:
view math explainer →
module
IndisputableMonolith.Constants
domain
Constants
line
219 · github
papers citing
1 paper (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants on GitHub at line 219.

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

 216/-! ### Canonical constants derived from φ -/
 217
 218/-- Canonical locked fine-structure constant: α_lock = (1 − 1/φ)/2. -/
 219@[simp] noncomputable def alphaLock : ℝ := (1 - 1 / phi) / 2
 220
 221/-- Useful bridge identity: the “acceleration-parameterized” exponent is `2·alphaLock`.
 222
 223This is purely algebraic (no physics): it just clears the `/2` in the definition. -/
 224lemma two_mul_alphaLock : 2 * alphaLock = 1 - 1 / phi := by
 225  unfold alphaLock
 226  ring_nf
 227
 228lemma alphaLock_pos : 0 < alphaLock := by
 229  have hphi := one_lt_phi
 230  unfold alphaLock
 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

papers checked against this theorem (showing 1 of 1)