`J_bit`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants on GitHub at line 249.

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

 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
 265All SI/CODATA anchoring is treated as **external calibration** and lives in
 266separate modules (e.g. `IndisputableMonolith.Constants.Consistency`,
 267`IndisputableMonolith.Constants.Derivation`, `IndisputableMonolith.Constants.Codata`,
 268and `IndisputableMonolith.Constants.RSNativeUnits`). -/
 269
 270/-- The fundamental time unit τ₀ (duration of one tick) in RS-native units. -/
 271@[simp] noncomputable def tau0 : ℝ := tick
 272
 273lemma tau0_pos : 0 < tau0 := by
 274  simp [tau0, tick]
 275
 276/-! ## C-004: Planck's Constant ħ Derivation
 277
 278### The RS Derivation of ħ
 279

papers checked against this theorem

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