`coherenceExponent`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.PlanckConstantFromRS
domain: Physics
line: 29 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.PlanckConstantFromRS on GitHub at line 29.

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

  26open Constants
  27
  28/-- Coherence exponent k=5. -/
  29def coherenceExponent : ℕ := 5
  30
  31/-- hbar = φ^(-5) in RS units. -/
  32noncomputable def hbar_RS : ℝ := (phi ^ coherenceExponent)⁻¹
  33
  34/-- hbar > 0. -/
  35theorem hbar_RS_pos : 0 < hbar_RS :=
  36  inv_pos.mpr (pow_pos phi_pos coherenceExponent)
  37
  38/-- G = φ^5/π in RS units. -/
  39noncomputable def G_RS : ℝ := phi ^ coherenceExponent / Real.pi
  40
  41/-- G > 0. -/
  42theorem G_RS_pos : 0 < G_RS :=
  43  div_pos (pow_pos phi_pos coherenceExponent) Real.pi_pos
  44
  45/-- κ = 8φ^5 in RS units. -/
  46noncomputable def kappa_RS : ℝ := 8 * phi ^ coherenceExponent
  47
  48theorem kappa_RS_pos : 0 < kappa_RS :=
  49  mul_pos (by norm_num) (pow_pos phi_pos coherenceExponent)
  50
  51/-- The Einstein relation κ = 8π G (verified structurally). -/
  52theorem einstein_relation : kappa_RS = 8 * Real.pi * G_RS := by
  53  unfold kappa_RS G_RS
  54  field_simp [Real.pi_ne_zero]
  55
  56structure PlanckConstantCert where
  57  exponent : coherenceExponent = 5
  58  hbar_pos : 0 < hbar_RS
  59  G_pos : 0 < G_RS

papers checked against this theorem

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