one_mem_phi_ladder

formal source

 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). -/
 530theorem Jcost_val_half : Cost.Jcost (1 / 2) = 1 / 4 := by
 531  unfold Cost.Jcost; norm_num
 532