`D_forces_eight_tick`

proved

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.Constants
domain: RRF
line: 66 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RRF.Foundation.Constants on GitHub at line 66.

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

formal source

  63def eight_tick : ℕ := 8
  64
  65/-- Dimension D = 3 forces 8-tick (2^D = 8). -/
  66theorem D_forces_eight_tick : 2 ^ 3 = eight_tick := by rfl
  67
  68/-! ## Speed of Light -/
  69
  70/-- c = ℓ₀ / τ₀ (derived from units, not measured).
  71
  72In RS: c is the ratio of fundamental length to fundamental time.
  73The SI value 299,792,458 m/s comes from calibration.
  74-/
  75noncomputable def c_SI : ℝ := 299792458
  76
  77/-! ## Planck Constant -/
  78
  79/-- ℏ = E_coh · τ₀ (the IR gate identity).
  80
  81This is not measured; it's derived from φ.
  82-/
  83noncomputable def hbar_derived (e_coh tau_0 : ℝ) : ℝ := e_coh * tau_0
  84
  85/-- The IR gate identity: ℏ = E_coh · τ₀. -/
  86theorem IR_gate_identity (e_coh tau_0 hbar : ℝ)
  87    (h : hbar = e_coh * tau_0) : hbar = hbar_derived e_coh tau_0 := by
  88  simp only [hbar_derived, h]
  89
  90/-! ## Fine Structure Constant -/
  91
  92/-- α⁻¹ derived from geometric seed (the claim, not yet proved).
  93
  94α⁻¹ = 128 · ln(π/2) + 45 · ln φ + curvature_correction
  95
  96Where:

papers checked against this theorem

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