RSReal_synth

formal source

 481  RSExists x ∧ x ∈ D
 482
 483/-- RSReal with synthesis map F : U → ℝ and discrete skeleton D ⊆ U. (Paper Eq. 9) -/
 484def RSReal_synth {U : Type*} (D : Set U) (F : U → ℝ) (x : ℝ) : Prop :=
 485  RSExists x ∧ ∃ u ∈ D, x = F u
 486
 487theorem RSReal_gen_at_one {D : Set ℝ} (hD : (1 : ℝ) ∈ D) : RSReal_gen D 1 :=
 488  ⟨rs_exists_one, hD⟩
 489
 490theorem RSReal_gen_iff {D : Set ℝ} {x : ℝ} :
 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