`phi_ladder`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.OntologyPredicates
domain: Foundation
line: 499 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.OntologyPredicates on GitHub at line 499.

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

 496  simp only [RSReal_synth, rs_exists_unique_one]
 497
 498/-- The φ-ladder as a specific discrete skeleton. -/
 499noncomputable def phi_ladder : Set ℝ :=
 500  {x | ∃ n : ℤ, x = PhiForcing.φ ^ n}
 501
 502theorem one_mem_phi_ladder : (1 : ℝ) ∈ phi_ladder :=
 503  ⟨0, by simp [PhiForcing.φ]⟩
 504
 505theorem RSReal_gen_phi_one : RSReal_gen phi_ladder 1 :=
 506  RSReal_gen_at_one one_mem_phi_ladder
 507
 508/-! ## Numeric Verification of Paper Examples (Section 4.1)
 509
 510The paper uses concrete J-cost values in Tables 1–3.
 511We verify each value used.
 512-/
 513
 514theorem Jcost_val_2 : Cost.Jcost 2 = 1 / 4 := by
 515  unfold Cost.Jcost; norm_num
 516
 517theorem Jcost_val_4 : Cost.Jcost 4 = 9 / 8 := by
 518  unfold Cost.Jcost; norm_num
 519
 520theorem Jcost_val_5 : Cost.Jcost 5 = 8 / 5 := by
 521  unfold Cost.Jcost; norm_num
 522
 523theorem Jcost_val_6 : Cost.Jcost 6 = 25 / 12 := by
 524  unfold Cost.Jcost; norm_num
 525
 526theorem Jcost_val_8 : Cost.Jcost 8 = 49 / 16 := by
 527  unfold Cost.Jcost; norm_num
 528
 529/-- J(1/2) = J(2) by reciprocal symmetry (used in Example 3). -/

papers checked against this theorem

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