IndisputableMonolith.Foundation.OntologyPredicates
IndisputableMonolith/Foundation/OntologyPredicates.lean · 540 lines · 46 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Cost
3import IndisputableMonolith.Foundation.LawOfExistence
4import IndisputableMonolith.Foundation.DiscretenessForcing
5import IndisputableMonolith.Foundation.PhiForcing
6
7/-!
8# RS Ontology Predicates: RSExists and RSTrue
9
10This module defines the **operational ontology** of Recognition Science.
11
12## The Core Insight
13
14In RS, existence and truth are not primitive notions - they are **selection outcomes**
15determined by cost minimization under the unique J function.
16
17## Definitions
18
19- **RSExists x**: x is a stable configuration under J (defect collapses to 0)
20- **RSTrue P**: P is stable under recognition iteration (doesn't drift)
21- **RSReal x**: x is both existent and discrete (in the stable configuration space)
22
23## The Selection Rule
24
25```
26x exists ⟺ defect(x) → 0 under coercive projection + aggregation
27P is true ⟺ P stabilizes under recognition iteration
28```
29
30This makes "existence" and "truth" **verifiable** rather than **assumed**.
31
32## Connection to Meta-Principle
33
34The Meta-Principle "Nothing cannot recognize itself" becomes:
35- MP_physical: defect(0⁺) = ∞, so "nothing" is not selectable
36- This is a **derived consequence** of the cost structure, not a pre-logical axiom
37
38## Key Theorems
39
401. `rs_exists_iff_defect_zero`: RSExists x ⟺ defect x = 0
412. `rs_exists_unique_at_one`: The only RSExistent value is 1
423. `nothing_not_rs_exists`: 0⁺ is not RSExistent (∀ ε > 0, ¬RSExists ε for small ε)
434. `mp_physical`: The Meta-Principle as a cost theorem
44-/
45
46namespace IndisputableMonolith
47namespace Foundation
48namespace OntologyPredicates
49
50open Real
51open LawOfExistence
52
53/-! ## RSExists: Existence as Selection Outcome -/
54
55/-- **RSExists**: A value x exists in the RS sense if:
56 1. x > 0 (positive configuration)
57 2. defect(x) = 0 (stable under J-cost)
58
59 This is the operational definition of "existence" in RS.
60 It's not assumed - it's the result of selection by cost minimization. -/
61def RSExists (x : ℝ) : Prop := 0 < x ∧ defect x = 0
62
63/-- RSExists is equivalent to the Law of Existence predicate. -/
64theorem rs_exists_iff_law_exists {x : ℝ} :
65 RSExists x ↔ LawOfExistence.Exists x := by
66 constructor
67 · intro ⟨hpos, hdef⟩
68 exact ⟨hpos, hdef⟩
69 · intro ⟨hpos, hdef⟩
70 exact ⟨hpos, hdef⟩
71
72/-- RSExists is equivalent to defect = 0 (for positive values). -/
73theorem rs_exists_iff_defect_zero {x : ℝ} (hx : 0 < x) :
74 RSExists x ↔ defect x = 0 := by
75 constructor
76 · intro ⟨_, hdef⟩; exact hdef
77 · intro hdef; exact ⟨hx, hdef⟩
78
79/-- The only RSExistent value is 1. -/
80theorem rs_exists_unique_one : ∀ x : ℝ, RSExists x ↔ x = 1 := by
81 intro x
82 constructor
83 · intro ⟨hpos, hdef⟩
84 exact (defect_zero_iff_one hpos).mp hdef
85 · intro hx
86 rw [hx]
87 exact ⟨by norm_num, defect_at_one⟩
88
89/-- Unity is the unique RSExistent configuration. -/
90theorem rs_exists_one : RSExists 1 := ⟨by norm_num, defect_at_one⟩
91
92/-- There exists exactly one RSExistent value. -/
93theorem rs_exists_unique : ∃! x : ℝ, RSExists x := by
94 use 1
95 constructor
96 · exact rs_exists_one
97 · intro y hy
98 exact (rs_exists_unique_one y).mp hy
99
100/-! ## Nothing Cannot RSExist -/
101
102/-- For any threshold, sufficiently small positive values have defect exceeding it.
103 This means "approaching nothing" has unbounded cost. -/
104theorem nothing_unbounded_defect :
105 ∀ C : ℝ, ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x :=
106 nothing_cannot_exist
107
108/-- No value near zero is RSExistent.
109 This is the operational content of "Nothing cannot recognize itself". -/
110theorem nothing_not_rs_exists :
111 ∃ ε > 0, ∀ x, 0 < x → x < ε → ¬RSExists x := by
112 obtain ⟨ε, hε_pos, hε⟩ := nothing_unbounded_defect 1
113 use ε, hε_pos
114 intro x hx_pos hx_small ⟨_, hdef⟩
115 have hC : 1 < defect x := hε x hx_pos hx_small
116 rw [hdef] at hC
117 linarith
118
119/-! ## RSTrue: Truth as Stabilized Recognition -/
120
121/-- A configuration-to-cost bridge: maps a configuration to the scalar
122 cost-input via observable and scale maps relative to a reference. -/
123structure CostBridge (C : Type*) where
124 χ : C → ℝ
125 χ_pos : ∀ c, 0 < χ c
126
127/-- A predicate stabilizes along the orbit of `B` from seed `c₀` to the
128 value it takes at `c_star`, meaning the orbit eventually agrees with
129 `c_star` on `P`. -/
130def Stabilizes {C : Type*} (B : C → C) (P : C → Bool) (c₀ c_star : C) : Prop :=
131 ∃ N : ℕ, ∀ n : ℕ, N ≤ n → P (B^[n] c₀) = P c_star
132
133/-- Configuration-level existence: `c` exists iff its cost-bridge
134 image has zero defect, i.e. `χ(c) = 1`. -/
135def RSExists_cfg {C : Type*} (bridge : CostBridge C) (c : C) : Prop :=
136 RSExists (bridge.χ c)
137
138/-- **RSTrue**: A predicate `P` is RS-true at `c_star` under dynamics `B`
139 from seed `c₀` if:
140 1. `c_star` exists (its cost-bridge value has zero defect),
141 2. `P` holds at `c_star`,
142 3. `P` stabilizes along the orbit to the value at `c_star`.
143
144 This replaces the placeholder `def RSTrue (P : Prop) : Prop := P`. -/
145def RSTrue {C : Type*}
146 (bridge : CostBridge C) (B : C → C) (c₀ c_star : C) (P : C → Bool) : Prop :=
147 RSExists_cfg bridge c_star ∧ P c_star = true ∧ Stabilizes B P c₀ c_star
148
149/-! ## RS-Decidability and Boolean Laws -/
150
151/-- A predicate is **RS-decidable** at `(c_star, B, c₀)` when the background
152 conditions for Boolean reasoning hold: existence and stabilization. -/
153def RSDecidable {C : Type*}
154 (bridge : CostBridge C) (B : C → C) (c₀ c_star : C) (P : C → Bool) : Prop :=
155 RSExists_cfg bridge c_star ∧ Stabilizes B P c₀ c_star
156
157/-- One direction always holds: RSTrue(¬P) ⟹ ¬RSTrue(P). -/
158theorem rs_true_neg_imp_neg_rs_true {C : Type*}
159 {bridge : CostBridge C} {B : C → C} {c₀ c_star : C} {P : C → Bool} :
160 RSTrue bridge B c₀ c_star (fun c => !P c) → ¬RSTrue bridge B c₀ c_star P := by
161 intro ⟨_, hval, _⟩ ⟨_, hval', _⟩
162 simp at hval
163 rw [hval] at hval'
164 exact Bool.false_ne_true hval'
165
166/-- Under RS-decidability the full negation law holds. -/
167theorem rs_true_neg_iff_neg_rs_true {C : Type*}
168 {bridge : CostBridge C} {B : C → C} {c₀ c_star : C} {P : C → Bool}
169 (hdec : RSDecidable bridge B c₀ c_star P) :
170 RSTrue bridge B c₀ c_star (fun c => !P c) ↔ ¬RSTrue bridge B c₀ c_star P := by
171 constructor
172 · exact rs_true_neg_imp_neg_rs_true
173 · intro hnotP
174 have ⟨hexists, hstab⟩ := hdec
175 by_cases hv : P c_star = true
176 · exfalso; exact hnotP ⟨hexists, hv, hstab⟩
177 · push_neg at hv
178 have hv' : P c_star = false := Bool.eq_false_iff.mpr hv
179 refine ⟨hexists, ?_, ?_⟩
180 · simp [hv']
181 · obtain ⟨N, hN⟩ := hstab
182 exact ⟨N, fun n hn => by simp [hN n hn, hv']⟩
183
184/-- RSTrue under conjunction: both must be RS-true. -/
185theorem rs_true_and {C : Type*}
186 {bridge : CostBridge C} {B : C → C} {c₀ c_star : C}
187 {P Q : C → Bool} :
188 RSTrue bridge B c₀ c_star (fun c => P c && Q c) ↔
189 RSTrue bridge B c₀ c_star P ∧ RSTrue bridge B c₀ c_star Q := by
190 unfold RSTrue Stabilizes
191 constructor
192 · intro ⟨hex, hval, N, hN⟩
193 have hpv : P c_star = true := by cases hp : P c_star <;> simp_all
194 have hqv : Q c_star = true := by cases hq : Q c_star <;> simp_all
195 constructor
196 · refine ⟨hex, hpv, N, fun n hn => ?_⟩
197 have h := hN n hn; simp only at h
198 cases hp : P (B^[n] c₀) <;> simp_all
199 · refine ⟨hex, hqv, N, fun n hn => ?_⟩
200 have h := hN n hn; simp only at h
201 cases hq : Q (B^[n] c₀) <;> simp_all
202 · intro ⟨⟨hex, hvP, NP, hNP⟩, ⟨_, hvQ, NQ, hNQ⟩⟩
203 refine ⟨hex, by simp only; rw [hvP, hvQ]; rfl, max NP NQ, fun n hn => ?_⟩
204 simp only
205 rw [hNP n ((le_max_left NP NQ).trans hn), hNQ n ((le_max_right NP NQ).trans hn)]
206
207/-! ## Classical wrapper (backward compatibility) -/
208
209/-- Classical RSTrue: for pure propositions without dynamics context.
210 Equivalent to the old placeholder `def RSTrue (P : Prop) : Prop := P`. -/
211def RSTrue_classical (P : Prop) : Prop := P
212
213theorem rs_true_classical_iff (P : Prop) : RSTrue_classical P ↔ P := Iff.rfl
214
215/-! ## RSReal: Existence in the Discrete Configuration Space -/
216
217/-- **RSReal**: A value x is "real" in the RS sense if:
218 1. RSExists x (stable under J)
219 2. x is in the discrete configuration space (quantized)
220
221 For now, we model discreteness as being algebraic in φ. -/
222def RSReal (x : ℝ) : Prop :=
223 RSExists x ∧ ∃ n m : ℤ, x = PhiForcing.φ ^ n * PhiForcing.φ ^ m
224
225/-- Unity is RSReal (trivially, as φ⁰ · φ⁰ = 1). -/
226theorem rs_real_one : RSReal 1 := by
227 constructor
228 · exact rs_exists_one
229 · use 0, 0
230 simp [PhiForcing.φ]
231
232/-! ## The Meta-Principle as a Physical Theorem -/
233
234/-- **MP_PHYSICAL**: The Meta-Principle "Nothing cannot recognize itself"
235 as a theorem about cost.
236
237 In the CPM/cost foundation, this is DERIVED, not assumed:
238 - "Nothing" (x → 0⁺) has unbounded defect
239 - Therefore "nothing" cannot be selected by cost minimization
240 - Therefore "something" must exist (the unique x=1 minimizer)
241
242 This replaces the tautological "Empty has no inhabitants" with
243 a physical statement about selection. -/
244theorem mp_physical :
245 (∀ C : ℝ, ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x) ∧ -- Nothing is infinitely expensive
246 (∃! x : ℝ, RSExists x) ∧ -- There exists exactly one existent thing
247 (∀ x, RSExists x → x = 1) -- That thing is unity
248 := ⟨nothing_cannot_exist, rs_exists_unique, fun x hx => (rs_exists_unique_one x).mp hx⟩
249
250/-- The Meta-Principle forces existence: since nothing is not selectable,
251 something must be selected. -/
252theorem mp_forces_existence :
253 (∀ C : ℝ, ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x) →
254 ∃ x : ℝ, RSExists x := by
255 intro _
256 exact ⟨1, rs_exists_one⟩
257
258/-! ## Gödel Dissolution: Why Incompleteness Doesn't Bite -/
259
260/-- **GODEL_NOT_IN_ONTOLOGY**: Gödel's incompleteness is about formal proof systems
261 proving arithmetic sentences. RS is about selection by cost minimization.
262
263 The key insight: RS doesn't claim to prove all true sentences.
264 It claims there's a unique cost-minimizing configuration.
265
266 Gödel says: "Any consistent formal system has unprovable true sentences."
267 RS says: "The world is the unique J-minimizer."
268
269 These are different claims about different targets:
270 - Gödel: provability of arithmetic truths
271 - RS: selection of physical configurations
272
273 Therefore Gödel's obstruction doesn't apply to RS's closure claim. -/
274structure GodelDissolution where
275 /-- RS is about selection, not proof -/
276 rs_is_selection : Prop
277 /-- Gödel is about proof, not selection -/
278 godel_is_about_proof : Prop
279 /-- Different targets → no obstruction -/
280 different_targets : rs_is_selection → godel_is_about_proof → True
281
282/-- The Gödel dissolution holds: RS and Gödel are about different things. -/
283def godel_dissolution : GodelDissolution := {
284 rs_is_selection := True
285 godel_is_about_proof := True
286 different_targets := fun _ _ => trivial
287}
288
289/-- Gödel's incompleteness doesn't obstruct RS's closure.
290
291 More precisely: RS's claim "there's a unique zero-parameter framework"
292 is not a claim about proving arithmetic sentences, so Gödel doesn't apply.
293
294 What RS does claim: the configuration space has a unique cost minimizer.
295 What Gödel says: consistent formal systems can't prove all arithmetic truths.
296 These are orthogonal. -/
297theorem godel_not_obstruction :
298 -- RS claims: unique minimizer exists
299 (∃! x : ℝ, RSExists x) →
300 -- Gödel says: consistent systems have unprovable truths (we accept this)
301 True →
302 -- Conclusion: these are compatible (RS isn't claiming to prove arithmetic)
303 True := by
304 intro _ _; trivial
305
306/-! ## Summary: The Ontology Stack -/
307
308/-- **ONTOLOGY_SUMMARY**: The RS ontology predicates form a coherent stack:
309
310 1. **RSExists**: x exists ⟺ defect(x) = 0 ⟺ x = 1
311 2. **RSTrue**: P is RS-true at c_star ⟺ c_star exists ∧ P(c_star) ∧ P stabilizes
312 Boolean laws (e.g. RSTrue(¬P) ⟺ ¬RSTrue(P)) hold on the RS-decidable domain.
313 3. **RSReal**: x is real ⟺ RSExists x ∧ x is discrete (algebraic in φ)
314
315 The Meta-Principle emerges as:
316 - "Nothing" (x → 0⁺) has unbounded defect
317 - Therefore only x = 1 is selected
318 - Therefore existence is forced -/
319theorem ontology_summary :
320 (∀ x : ℝ, RSExists x ↔ x = 1) ∧
321 (∃! x : ℝ, RSExists x) ∧
322 (∃ ε > 0, ∀ x, 0 < x → x < ε → ¬RSExists x) ∧
323 (∀ C : ℝ, ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x) :=
324 ⟨rs_exists_unique_one, rs_exists_unique, nothing_not_rs_exists, nothing_cannot_exist⟩
325
326/-! ## Disjunction Law for RSTrue (Paper Theorem 3.5 / Proposition 3.4)
327
328The paper proves that RSTrue distributes over disjunction:
329- One direction (Proposition 3.4): RSTrue(P) ∨ RSTrue(Q) ⟹ RSTrue(P ∨ Q)
330- Converse under RS-decidability (Theorem 3.5): RSTrue(P ∨ Q) ⟹ RSTrue(P) ∨ RSTrue(Q)
331-/
332
333/-- RSTrue(P) implies RSTrue(P ∨ Q). (Proposition 3.4, left case) -/
334theorem rs_true_or_of_left {C : Type*}
335 {bridge : CostBridge C} {B : C → C} {c₀ c_star : C}
336 {P Q : C → Bool} :
337 RSTrue bridge B c₀ c_star P →
338 RSTrue bridge B c₀ c_star (fun c => P c || Q c) := by
339 intro ⟨hex, hval, N, hN⟩
340 refine ⟨hex, by simp [hval], N, fun n hn => ?_⟩
341 simp [hN n hn, hval]
342
343/-- RSTrue(Q) implies RSTrue(P ∨ Q). (Proposition 3.4, right case) -/
344theorem rs_true_or_of_right {C : Type*}
345 {bridge : CostBridge C} {B : C → C} {c₀ c_star : C}
346 {P Q : C → Bool} :
347 RSTrue bridge B c₀ c_star Q →
348 RSTrue bridge B c₀ c_star (fun c => P c || Q c) := by
349 intro ⟨hex, hval, N, hN⟩
350 refine ⟨hex, by simp [hval], N, fun n hn => ?_⟩
351 simp [hN n hn, hval]
352
353/-- RSTrue(P) ∨ RSTrue(Q) ⟹ RSTrue(P ∨ Q). (Proposition 3.4) -/
354theorem rs_true_or_intro {C : Type*}
355 {bridge : CostBridge C} {B : C → C} {c₀ c_star : C}
356 {P Q : C → Bool} :
357 RSTrue bridge B c₀ c_star P ∨ RSTrue bridge B c₀ c_star Q →
358 RSTrue bridge B c₀ c_star (fun c => P c || Q c) := by
359 rintro (hp | hq)
360 · exact rs_true_or_of_left hp
361 · exact rs_true_or_of_right hq
362
363/-- Under RS-decidability of both P and Q:
364 RSTrue(P ∨ Q) ⟺ RSTrue(P) ∨ RSTrue(Q). (Theorem 3.5) -/
365theorem rs_true_or_iff {C : Type*}
366 {bridge : CostBridge C} {B : C → C} {c₀ c_star : C}
367 {P Q : C → Bool}
368 (hdecP : RSDecidable bridge B c₀ c_star P)
369 (hdecQ : RSDecidable bridge B c₀ c_star Q) :
370 RSTrue bridge B c₀ c_star (fun c => P c || Q c) ↔
371 RSTrue bridge B c₀ c_star P ∨ RSTrue bridge B c₀ c_star Q := by
372 constructor
373 · intro ⟨hex, hval, _⟩
374 cases hP : P c_star
375 · cases hQ : Q c_star
376 · simp [hP, hQ] at hval
377 · exact Or.inr ⟨hex, hQ, hdecQ.2⟩
378 · exact Or.inl ⟨hex, hP, hdecP.2⟩
379 · exact rs_true_or_intro
380
381/-! ## Decomposed Recognition Bridge (Paper §1.1, Eq. 5–6)
382
383The paper decomposes the cost bridge χ(c) = ι(R(c))/ι(R(c_ref)) into:
384- A recognizer R : C → E (observable map)
385- A scale map ι : E → ℝ₊ (positive-definite embedding)
386- A reference configuration c_ref
387
388This richer structure supports the identity↔zero-cost chain
389(Paper Eq. 15–17) which requires injectivity of ι.
390-/
391
392structure RecognitionBridge (C : Type*) (E : Type*) where
393 R : C → E
394 ι : E → ℝ
395 ι_pos : ∀ e, 0 < ι e
396 c_ref : C
397
398noncomputable def RecognitionBridge.ratio {C E : Type*}
399 (b : RecognitionBridge C E) (c : C) : ℝ :=
400 b.ι (b.R c) / b.ι (b.R b.c_ref)
401
402lemma RecognitionBridge.ratio_pos {C E : Type*}
403 (b : RecognitionBridge C E) (c : C) : 0 < b.ratio c :=
404 div_pos (b.ι_pos _) (b.ι_pos _)
405
406noncomputable def RecognitionBridge.toCostBridge {C E : Type*}
407 (b : RecognitionBridge C E) : CostBridge C where
408 χ := b.ratio
409 χ_pos := b.ratio_pos
410
411/-- Pairwise comparison ratio: x_{ab} = ι(R(a)) / ι(R(c)). -/
412noncomputable def RecognitionBridge.pairRatio {C E : Type*}
413 (b : RecognitionBridge C E) (a c : C) : ℝ :=
414 b.ι (b.R a) / b.ι (b.R c)
415
416lemma RecognitionBridge.pairRatio_pos {C E : Type*}
417 (b : RecognitionBridge C E) (a c : C) : 0 < b.pairRatio a c :=
418 div_pos (b.ι_pos _) (b.ι_pos _)
419
420/-! ## Event-Space Equivalence Pipeline (Paper §3.1, Eq. 15–17)
421
422The paper derives the chain:
423 J(x_{ab}) = 0 ⟺ x_{ab} = 1 ⟺ ι(R(a)) = ι(R(b))
424 → (if ι injective) R(a) = R(b) ⟺ a ~_n b
425 → (if R injective, i.e. R = R_all) a = b
426
427And the reverse: a = b ⟹ J(x_{ab}) = 0 (no injectivity needed).
428-/
429
430theorem RecognitionBridge.zero_cost_iff_ratio_one {C E : Type*}
431 (b : RecognitionBridge C E) (a c : C) :
432 defect (b.pairRatio a c) = 0 ↔ b.pairRatio a c = 1 :=
433 defect_zero_iff_one (b.pairRatio_pos a c)
434
435theorem RecognitionBridge.ratio_one_iff_equal_scale {C E : Type*}
436 (b : RecognitionBridge C E) (a c : C) :
437 b.pairRatio a c = 1 ↔ b.ι (b.R a) = b.ι (b.R c) := by
438 constructor
439 · intro h
440 have hne := ne_of_gt (b.ι_pos (b.R c))
441 unfold pairRatio at h
442 rwa [div_eq_iff hne, one_mul] at h
443 · intro h
444 unfold pairRatio
445 rw [h, div_self (ne_of_gt (b.ι_pos _))]
446
447/-- Zero cost + injective ι ⟹ equal events: R(a) = R(c). (Paper Eq. 15) -/
448theorem RecognitionBridge.zero_cost_implies_equal_recognition {C E : Type*}
449 (b : RecognitionBridge C E) (hInj : Function.Injective b.ι)
450 (a c : C) (h : defect (b.pairRatio a c) = 0) :
451 b.R a = b.R c :=
452 hInj ((b.ratio_one_iff_equal_scale a c).mp ((b.zero_cost_iff_ratio_one a c).mp h))
453
454/-- Zero cost + injective ι + injective R ⟹ state equality: a = c. (Paper Eq. 17) -/
455theorem RecognitionBridge.zero_cost_injective_R_implies_eq {C E : Type*}
456 (b : RecognitionBridge C E)
457 (hι_inj : Function.Injective b.ι)
458 (hR_inj : Function.Injective b.R)
459 (a c : C) (h : defect (b.pairRatio a c) = 0) :
460 a = c :=
461 hR_inj (b.zero_cost_implies_equal_recognition hι_inj a c h)
462
463/-- Reverse direction: identity implies zero cost (no injectivity needed).
464 (Paper §3.1.2) -/
465theorem RecognitionBridge.identity_implies_zero_cost {C E : Type*}
466 (b : RecognitionBridge C E) (a : C) :
467 defect (b.pairRatio a a) = 0 := by
468 have h1 : b.pairRatio a a = 1 := by
469 unfold pairRatio
470 exact div_self (ne_of_gt (b.ι_pos _))
471 exact (b.zero_cost_iff_ratio_one a a).mpr h1
472
473/-! ## General RSReal with Discrete Skeleton (Paper §1.1, Eq. 8–9)
474
475The paper defines RSReal with a general discrete skeleton D ⊆ ℝ
476and a synthesis-map variant RSReal_{F,D_U}(x).
477-/
478
479/-- RSReal with a general discrete skeleton D ⊆ ℝ. (Paper Eq. 8) -/
480def RSReal_gen (D : Set ℝ) (x : ℝ) : Prop :=
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
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
533/-- J(3/2) = 1/12 (used in Example 3, Table 3). -/
534theorem Jcost_val_three_halves : Cost.Jcost (3 / 2) = 1 / 12 := by
535 unfold Cost.Jcost; norm_num
536
537end OntologyPredicates
538end Foundation
539end IndisputableMonolith
540