`cycleLength`

definition

show as: view math explainer →

module: IndisputableMonolith.Derivations.MassToLight
domain: Derivations
line: 183 · 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 183.

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

 180/-! ## Ledger Budget Derivation -/
 181
 182/-- Events in the 8-tick cycle. -/
 183def cycleLength : ℕ := 8
 184
 185/-- Mass-accumulation ticks in one cycle. -/
 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

papers checked against this theorem

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