RSReal_synth_iff

formal source

 491    RSReal_gen D x ↔ x = 1 ∧ x ∈ D := by
 492  simp only [RSReal_gen, rs_exists_unique_one]
 493
 494theorem RSReal_synth_iff {U : Type*} {D : Set U} {F : U → ℝ} {x : ℝ} :
 495    RSReal_synth D F x ↔ x = 1 ∧ ∃ u ∈ D, x = F u := by
 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