IndisputableMonolith.Foundation.OntologyPredicates
IndisputableMonolith/Foundation/OntologyPredicates.lean · 566 lines · 49 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/-! ## Categorical Distinctness Between RS Closure and Gödel I
259
260The two structures below are **documentation records, not theorems**.
261Their fields are `Prop` placeholders; the canonical inhabitants set every
262field to `True`. They package the philosophical/categorical claim that
263the RS closure question (uniqueness of the cost minimizer) and Gödel I
264(incompleteness of recursively axiomatized arithmetic) are about
265different objects.
266
267The historical naming (`GodelDissolution`, `godel_dissolution`,
268`godel_not_obstruction`) overstated what is recorded here. None of these
269declarations is a refutation of Gödel I or a proof that RS escapes
270incompleteness. The substantive argument lives in the prose of
271`papers/Godel_And_RS_Closure_Honest_Assessment_20260520.html` and is a
272meta-level categorical claim, not a Lean theorem.
273
274The companion arithmetic-recovery paper
275(`papers/RS_Arithmetic_From_Law_Of_Logic.pdf`) and the functional-equation
276paper (`Logic_Functional_Equation.tex`) state the honest position: the
277recovered arithmetic inherits incompleteness from Gödel I; RS closure
278(uniqueness of the J-minimum and the forcing chain to constants) is a
279categorically different question, not affected by incompleteness of the
280downstream arithmetic theory.
281-/
282
283/-- Documentation record: RS closure and Gödel I target different objects.
284Each field is a `Prop` placeholder; the canonical inhabitant has every
285field set to `True`. Not a theorem. -/
286structure RsAndGodelCategoricalDistinctness where
287 /-- RS closure is about selection / uniqueness of cost minimum. -/
288 rs_is_selection : Prop
289 /-- Gödel I is about provability inside recursively axiomatized arithmetic. -/
290 godel_is_about_proof : Prop
291 /-- These are categorically different targets; one does not bear on the
292 other in the direct sense. -/
293 different_targets : rs_is_selection → godel_is_about_proof → True
294
295/-- Canonical inhabitant of `RsAndGodelCategoricalDistinctness` with each
296philosophical field set to `True`. Documentation, not a theorem. -/
297def rs_and_godel_categorical_distinctness : RsAndGodelCategoricalDistinctness := {
298 rs_is_selection := True
299 godel_is_about_proof := True
300 different_targets := fun _ _ => trivial
301}
302
303/-- **Deprecated.** Renamed to `RsAndGodelCategoricalDistinctness`. -/
304@[deprecated "Renamed to RsAndGodelCategoricalDistinctness" (since := "2026-05-20")]
305abbrev GodelDissolution := RsAndGodelCategoricalDistinctness
306
307/-- **Deprecated.** Renamed to `rs_and_godel_categorical_distinctness`. -/
308@[deprecated "Renamed to rs_and_godel_categorical_distinctness" (since := "2026-05-20")]
309def godel_dissolution : RsAndGodelCategoricalDistinctness :=
310 rs_and_godel_categorical_distinctness
311
312/-- Vacuous statement (`True → True`): given uniqueness of the RS existent,
313no obstruction is derived from a trivial Gödel premise. The body is
314`fun _ _ => trivial`; there is no theorem content here. The historical
315name `godel_not_obstruction` overstated what this records.
316
317The honest version of this claim ("Gödel I does not directly target the
318RS forcing chain") is meta-level prose, not a Lean theorem. -/
319theorem rs_closure_vacuous_under_godel_premise :
320 (∃! x : ℝ, RSExists x) →
321 True →
322 True := by
323 intro _ _; trivial
324
325/-- **Deprecated.** Renamed to `rs_closure_vacuous_under_godel_premise`. -/
326@[deprecated "Renamed to rs_closure_vacuous_under_godel_premise" (since := "2026-05-20")]
327theorem godel_not_obstruction :
328 (∃! x : ℝ, RSExists x) →
329 True →
330 True := rs_closure_vacuous_under_godel_premise
331
332/-! ## Summary: The Ontology Stack -/
333
334/-- **ONTOLOGY_SUMMARY**: The RS ontology predicates form a coherent stack:
335
336 1. **RSExists**: x exists ⟺ defect(x) = 0 ⟺ x = 1
337 2. **RSTrue**: P is RS-true at c_star ⟺ c_star exists ∧ P(c_star) ∧ P stabilizes
338 Boolean laws (e.g. RSTrue(¬P) ⟺ ¬RSTrue(P)) hold on the RS-decidable domain.
339 3. **RSReal**: x is real ⟺ RSExists x ∧ x is discrete (algebraic in φ)
340
341 The Meta-Principle emerges as:
342 - "Nothing" (x → 0⁺) has unbounded defect
343 - Therefore only x = 1 is selected
344 - Therefore existence is forced -/
345theorem ontology_summary :
346 (∀ x : ℝ, RSExists x ↔ x = 1) ∧
347 (∃! x : ℝ, RSExists x) ∧
348 (∃ ε > 0, ∀ x, 0 < x → x < ε → ¬RSExists x) ∧
349 (∀ C : ℝ, ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x) :=
350 ⟨rs_exists_unique_one, rs_exists_unique, nothing_not_rs_exists, nothing_cannot_exist⟩
351
352/-! ## Disjunction Law for RSTrue (Paper Theorem 3.5 / Proposition 3.4)
353
354The paper proves that RSTrue distributes over disjunction:
355- One direction (Proposition 3.4): RSTrue(P) ∨ RSTrue(Q) ⟹ RSTrue(P ∨ Q)
356- Converse under RS-decidability (Theorem 3.5): RSTrue(P ∨ Q) ⟹ RSTrue(P) ∨ RSTrue(Q)
357-/
358
359/-- RSTrue(P) implies RSTrue(P ∨ Q). (Proposition 3.4, left case) -/
360theorem rs_true_or_of_left {C : Type*}
361 {bridge : CostBridge C} {B : C → C} {c₀ c_star : C}
362 {P Q : C → Bool} :
363 RSTrue bridge B c₀ c_star P →
364 RSTrue bridge B c₀ c_star (fun c => P c || Q c) := by
365 intro ⟨hex, hval, N, hN⟩
366 refine ⟨hex, by simp [hval], N, fun n hn => ?_⟩
367 simp [hN n hn, hval]
368
369/-- RSTrue(Q) implies RSTrue(P ∨ Q). (Proposition 3.4, right case) -/
370theorem rs_true_or_of_right {C : Type*}
371 {bridge : CostBridge C} {B : C → C} {c₀ c_star : C}
372 {P Q : C → Bool} :
373 RSTrue bridge B c₀ c_star Q →
374 RSTrue bridge B c₀ c_star (fun c => P c || Q c) := by
375 intro ⟨hex, hval, N, hN⟩
376 refine ⟨hex, by simp [hval], N, fun n hn => ?_⟩
377 simp [hN n hn, hval]
378
379/-- RSTrue(P) ∨ RSTrue(Q) ⟹ RSTrue(P ∨ Q). (Proposition 3.4) -/
380theorem rs_true_or_intro {C : Type*}
381 {bridge : CostBridge C} {B : C → C} {c₀ c_star : C}
382 {P Q : C → Bool} :
383 RSTrue bridge B c₀ c_star P ∨ RSTrue bridge B c₀ c_star Q →
384 RSTrue bridge B c₀ c_star (fun c => P c || Q c) := by
385 rintro (hp | hq)
386 · exact rs_true_or_of_left hp
387 · exact rs_true_or_of_right hq
388
389/-- Under RS-decidability of both P and Q:
390 RSTrue(P ∨ Q) ⟺ RSTrue(P) ∨ RSTrue(Q). (Theorem 3.5) -/
391theorem rs_true_or_iff {C : Type*}
392 {bridge : CostBridge C} {B : C → C} {c₀ c_star : C}
393 {P Q : C → Bool}
394 (hdecP : RSDecidable bridge B c₀ c_star P)
395 (hdecQ : RSDecidable bridge B c₀ c_star Q) :
396 RSTrue bridge B c₀ c_star (fun c => P c || Q c) ↔
397 RSTrue bridge B c₀ c_star P ∨ RSTrue bridge B c₀ c_star Q := by
398 constructor
399 · intro ⟨hex, hval, _⟩
400 cases hP : P c_star
401 · cases hQ : Q c_star
402 · simp [hP, hQ] at hval
403 · exact Or.inr ⟨hex, hQ, hdecQ.2⟩
404 · exact Or.inl ⟨hex, hP, hdecP.2⟩
405 · exact rs_true_or_intro
406
407/-! ## Decomposed Recognition Bridge (Paper §1.1, Eq. 5–6)
408
409The paper decomposes the cost bridge χ(c) = ι(R(c))/ι(R(c_ref)) into:
410- A recognizer R : C → E (observable map)
411- A scale map ι : E → ℝ₊ (positive-definite embedding)
412- A reference configuration c_ref
413
414This richer structure supports the identity↔zero-cost chain
415(Paper Eq. 15–17) which requires injectivity of ι.
416-/
417
418structure RecognitionBridge (C : Type*) (E : Type*) where
419 R : C → E
420 ι : E → ℝ
421 ι_pos : ∀ e, 0 < ι e
422 c_ref : C
423
424noncomputable def RecognitionBridge.ratio {C E : Type*}
425 (b : RecognitionBridge C E) (c : C) : ℝ :=
426 b.ι (b.R c) / b.ι (b.R b.c_ref)
427
428lemma RecognitionBridge.ratio_pos {C E : Type*}
429 (b : RecognitionBridge C E) (c : C) : 0 < b.ratio c :=
430 div_pos (b.ι_pos _) (b.ι_pos _)
431
432noncomputable def RecognitionBridge.toCostBridge {C E : Type*}
433 (b : RecognitionBridge C E) : CostBridge C where
434 χ := b.ratio
435 χ_pos := b.ratio_pos
436
437/-- Pairwise comparison ratio: x_{ab} = ι(R(a)) / ι(R(c)). -/
438noncomputable def RecognitionBridge.pairRatio {C E : Type*}
439 (b : RecognitionBridge C E) (a c : C) : ℝ :=
440 b.ι (b.R a) / b.ι (b.R c)
441
442lemma RecognitionBridge.pairRatio_pos {C E : Type*}
443 (b : RecognitionBridge C E) (a c : C) : 0 < b.pairRatio a c :=
444 div_pos (b.ι_pos _) (b.ι_pos _)
445
446/-! ## Event-Space Equivalence Pipeline (Paper §3.1, Eq. 15–17)
447
448The paper derives the chain:
449 J(x_{ab}) = 0 ⟺ x_{ab} = 1 ⟺ ι(R(a)) = ι(R(b))
450 → (if ι injective) R(a) = R(b) ⟺ a ~_n b
451 → (if R injective, i.e. R = R_all) a = b
452
453And the reverse: a = b ⟹ J(x_{ab}) = 0 (no injectivity needed).
454-/
455
456theorem RecognitionBridge.zero_cost_iff_ratio_one {C E : Type*}
457 (b : RecognitionBridge C E) (a c : C) :
458 defect (b.pairRatio a c) = 0 ↔ b.pairRatio a c = 1 :=
459 defect_zero_iff_one (b.pairRatio_pos a c)
460
461theorem RecognitionBridge.ratio_one_iff_equal_scale {C E : Type*}
462 (b : RecognitionBridge C E) (a c : C) :
463 b.pairRatio a c = 1 ↔ b.ι (b.R a) = b.ι (b.R c) := by
464 constructor
465 · intro h
466 have hne := ne_of_gt (b.ι_pos (b.R c))
467 unfold pairRatio at h
468 rwa [div_eq_iff hne, one_mul] at h
469 · intro h
470 unfold pairRatio
471 rw [h, div_self (ne_of_gt (b.ι_pos _))]
472
473/-- Zero cost + injective ι ⟹ equal events: R(a) = R(c). (Paper Eq. 15) -/
474theorem RecognitionBridge.zero_cost_implies_equal_recognition {C E : Type*}
475 (b : RecognitionBridge C E) (hInj : Function.Injective b.ι)
476 (a c : C) (h : defect (b.pairRatio a c) = 0) :
477 b.R a = b.R c :=
478 hInj ((b.ratio_one_iff_equal_scale a c).mp ((b.zero_cost_iff_ratio_one a c).mp h))
479
480/-- Zero cost + injective ι + injective R ⟹ state equality: a = c. (Paper Eq. 17) -/
481theorem RecognitionBridge.zero_cost_injective_R_implies_eq {C E : Type*}
482 (b : RecognitionBridge C E)
483 (hι_inj : Function.Injective b.ι)
484 (hR_inj : Function.Injective b.R)
485 (a c : C) (h : defect (b.pairRatio a c) = 0) :
486 a = c :=
487 hR_inj (b.zero_cost_implies_equal_recognition hι_inj a c h)
488
489/-- Reverse direction: identity implies zero cost (no injectivity needed).
490 (Paper §3.1.2) -/
491theorem RecognitionBridge.identity_implies_zero_cost {C E : Type*}
492 (b : RecognitionBridge C E) (a : C) :
493 defect (b.pairRatio a a) = 0 := by
494 have h1 : b.pairRatio a a = 1 := by
495 unfold pairRatio
496 exact div_self (ne_of_gt (b.ι_pos _))
497 exact (b.zero_cost_iff_ratio_one a a).mpr h1
498
499/-! ## General RSReal with Discrete Skeleton (Paper §1.1, Eq. 8–9)
500
501The paper defines RSReal with a general discrete skeleton D ⊆ ℝ
502and a synthesis-map variant RSReal_{F,D_U}(x).
503-/
504
505/-- RSReal with a general discrete skeleton D ⊆ ℝ. (Paper Eq. 8) -/
506def RSReal_gen (D : Set ℝ) (x : ℝ) : Prop :=
507 RSExists x ∧ x ∈ D
508
509/-- RSReal with synthesis map F : U → ℝ and discrete skeleton D ⊆ U. (Paper Eq. 9) -/
510def RSReal_synth {U : Type*} (D : Set U) (F : U → ℝ) (x : ℝ) : Prop :=
511 RSExists x ∧ ∃ u ∈ D, x = F u
512
513theorem RSReal_gen_at_one {D : Set ℝ} (hD : (1 : ℝ) ∈ D) : RSReal_gen D 1 :=
514 ⟨rs_exists_one, hD⟩
515
516theorem RSReal_gen_iff {D : Set ℝ} {x : ℝ} :
517 RSReal_gen D x ↔ x = 1 ∧ x ∈ D := by
518 simp only [RSReal_gen, rs_exists_unique_one]
519
520theorem RSReal_synth_iff {U : Type*} {D : Set U} {F : U → ℝ} {x : ℝ} :
521 RSReal_synth D F x ↔ x = 1 ∧ ∃ u ∈ D, x = F u := by
522 simp only [RSReal_synth, rs_exists_unique_one]
523
524/-- The φ-ladder as a specific discrete skeleton. -/
525noncomputable def phi_ladder : Set ℝ :=
526 {x | ∃ n : ℤ, x = PhiForcing.φ ^ n}
527
528theorem one_mem_phi_ladder : (1 : ℝ) ∈ phi_ladder :=
529 ⟨0, by simp [PhiForcing.φ]⟩
530
531theorem RSReal_gen_phi_one : RSReal_gen phi_ladder 1 :=
532 RSReal_gen_at_one one_mem_phi_ladder
533
534/-! ## Numeric Verification of Paper Examples (Section 4.1)
535
536The paper uses concrete J-cost values in Tables 1–3.
537We verify each value used.
538-/
539
540theorem Jcost_val_2 : Cost.Jcost 2 = 1 / 4 := by
541 unfold Cost.Jcost; norm_num
542
543theorem Jcost_val_4 : Cost.Jcost 4 = 9 / 8 := by
544 unfold Cost.Jcost; norm_num
545
546theorem Jcost_val_5 : Cost.Jcost 5 = 8 / 5 := by
547 unfold Cost.Jcost; norm_num
548
549theorem Jcost_val_6 : Cost.Jcost 6 = 25 / 12 := by
550 unfold Cost.Jcost; norm_num
551
552theorem Jcost_val_8 : Cost.Jcost 8 = 49 / 16 := by
553 unfold Cost.Jcost; norm_num
554
555/-- J(1/2) = J(2) by reciprocal symmetry (used in Example 3). -/
556theorem Jcost_val_half : Cost.Jcost (1 / 2) = 1 / 4 := by
557 unfold Cost.Jcost; norm_num
558
559/-- J(3/2) = 1/12 (used in Example 3, Table 3). -/
560theorem Jcost_val_three_halves : Cost.Jcost (3 / 2) = 1 / 12 := by
561 unfold Cost.Jcost; norm_num
562
563end OntologyPredicates
564end Foundation
565end IndisputableMonolith
566