`lightPhase`

definition

show as: view math explainer →

module: IndisputableMonolith.Derivations.MassToLight
domain: Derivations
line: 189 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Derivations.MassToLight on GitHub at line 189.

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

 186def massPhase : ℕ := 5
 187
 188/-- Light-emission ticks in one cycle. -/
 189def lightPhase : ℕ := 3
 190
 191/-- The phase ratio is determined by ledger topology. -/
 192theorem phase_ratio_from_topology :
 193    massPhase + lightPhase = cycleLength := by
 194  norm_num [massPhase, lightPhase, cycleLength]
 195
 196/-- M/L inherits the φ structure from phase ratios. -/
 197theorem ml_from_phase_ratio :
 198    (massPhase : ℝ) / (lightPhase : ℝ) = 5 / 3 := by
 199  norm_num [massPhase, lightPhase]
 200
 201/-! ## Consistency Check -/
 202
 203/-- The derived M/L is consistent with observations. -/
 204theorem ml_consistent_with_observation :
 205    ∃ n : ℤ, n ∈ Set.Icc 10 13 ∧
 206    -- The derived value φⁿ falls within observed range (100-550)
 207    (phi_power n > 100) ∧ (phi_power n < 550) := by
 208  use 10
 209  constructor
 210  · simp [Set.mem_Icc]
 211  constructor
 212  · exact phi_10_bounds
 213  · -- phi^10 < phi^13 < 550
 214    have h : phi_power 10 < phi_power 13 := by
 215      unfold phi_power
 216      apply zpow_lt_zpow_of_one_lt phi_gt_one (by norm_num)
 217    exact lt_trans h phi_13_bounds
 218
 219/-! ## Main Theorem: M/L is Derived, Not Input -/

papers checked against this theorem

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