`ml_consistent_with_observation`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Derivations.MassToLight on GitHub at line 204.

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

 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 -/
 220
 221theorem ml_is_derived_not_input :
 222    ∃ (derive : ℕ → ℤ → ℝ),
 223    (derive cycleLength = phi_power) ∧
 224    (∃ n : ℤ, derive cycleLength n > 100 ∧ derive cycleLength n < 550) := by
 225  use fun _ n => phi_power n
 226  constructor
 227  · rfl
 228  · use 10
 229    constructor
 230    · exact phi_10_bounds
 231    · exact lt_trans (by
 232        unfold phi_power
 233        apply zpow_lt_zpow_of_one_lt phi_gt_one (by norm_num)
 234      ) phi_13_bounds

papers checked against this theorem

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