IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostStructuralLedger
IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean · 1577 lines · 104 declarations
show as:
view math explainer →
1/-
2 PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean
3
4 Round-trip source:
5 plans/Delta_JCost_FreeSide_Program_Plan_20260724.html
6
7 The judge for everything below is `lake`. There is no preregistered empirical
8 gate here and none is claimed: these are kernel-checked theorems, and the
9 countermodels are exhibited functions, not measurements.
10
11 Rounds 4 to 6 of P-delta-jfree: replace the free-side calibration ledger by a
12 STRUCTURAL ledger. Rounds 1 to 3 proved that the slim ledger forces the
13 canonical cost on `RatioOrbit` and that it is field-by-field minimal, but four
14 of its eight fields are of the form "F agrees with J here", one of them over
15 the infinite family of prime pairs. This module removes the two substantive
16 ones and replaces them with statements about what a cost IS:
17
18 * SIGN REVERSAL (round 4). `PRCNativeCostSignReversing`: reversing the
19 orientation of a distinction negates its doubled trace, i.e. the display
20 identity `F(-q) = -F(q) - 2`. This is ledger antisymmetry (a debit read
21 backwards is a credit). Applied at the unit it DERIVES the signed-unit
22 calibration, so `signed_unit` leaves the ledger.
23
24 * MONOTONICITY (round 5). `PRCNativeCostMonotone`: on positive integer
25 orbits, a larger imbalance costs at least as much. This replaces the whole
26 prime-pair product family. The mathematics is Erdős 1946 (a monotone
27 completely additive arithmetic function is `c log n`), and in the
28 completely multiplicative case the proof is a squeeze on integer exponents
29 with no analysis in it: if `2^m ≤ a^n` then monotonicity transports the
30 inequality to the character values, so the character value at `a` cuts the
31 powers of two exactly where `a` does, and two positive rationals with the
32 same cut are equal. `cut_pins` below is that argument, stated with no
33 logarithm, no limit, and no real number anywhere.
34
35 What survives is `two_calibrated`, and round 6 shows that what survives is
36 exactly a UNIT GAUGE and not a hidden assumption of the answer:
37
38 * `structural_gauge_rigidity`: two inhabitants of the anchor-free structural
39 ledger that agree at the single orbit `2` agree on every orbit.
40 * `cubeGeneratedNativeCost`: the cost `J(q³)` inhabits the anchor-free
41 structural ledger and fails the anchor, so the gauge orbit is genuinely
42 inhabited and the anchor is a real choice rather than a redundancy. (The
43 Liouville and two-adic impostors of round 3 are NOT monotone, so they do
44 not witness this; the odd power family is what is left.)
45
46 Read together: on the countable carrier the FORM of the cost is forced by
47 arithmetic (reciprocity, normalization invariance, the composition law,
48 unit-zero, sign reversal, monotonicity, and the zero-orbit convention), and
49 the only residual freedom is the size of the unit, fixed by one anchor. That
50 is the same stratification the continuous theorem delivers, obtained without
51 buying continuity, smoothness, or the completed line.
52
53 Scope: reads the round-1/2/3 modules and the parent. It edits none of them.
54-/
55
56import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimalityCertificate
57
58namespace IndisputableMonolith
59namespace Foundation
60namespace PrimitiveRecognitionCalculus
61namespace PRCJCost
62
63/-! ## Part 0: the cost display on rationals
64
65Everything below is stated on displays (`RatioOrbit.toRat`), which is legitimate
66because `crossEq a b ↔ a.toRat = b.toRat`. -/
67
68/-- Read a cross-equivalence as an equality of displays. -/
69theorem crossDisp {a b : RatioOrbit} (h : RatioOrbit.crossEq a b) :
70 a.toRat = b.toRat := (RatioOrbit.crossEq_iff_toRat_eq a b).mp h
71
72/-- Read an equality of displays as a cross-equivalence. -/
73theorem dispCross {a b : RatioOrbit} (h : a.toRat = b.toRat) :
74 RatioOrbit.crossEq a b := (RatioOrbit.crossEq_iff_toRat_eq a b).mpr h
75
76/-- The J display on a rational. -/
77def jq (t : ℚ) : ℚ := (t + t⁻¹) / 2 - 1
78
79@[simp] theorem jq_onRatioOrbit (q : RatioOrbit) :
80 (onRatioOrbit q).toRat = jq q.toRat := onRatioOrbit_toRat q
81
82theorem costFromCharacter_jq (χ : RatioOrbit → RatioOrbit) (q : RatioOrbit) :
83 (costFromCharacter χ q).toRat = jq ((χ q).toRat) := costFromCharacter_toRat χ q
84
85@[simp] theorem jq_one : jq 1 = 0 := by norm_num [jq]
86
87@[simp] theorem jq_zero : jq 0 = -1 := by norm_num [jq]
88
89theorem jq_closed {t : ℚ} (ht : t ≠ 0) : jq t = (t - 1) ^ 2 / (2 * t) := by
90 unfold jq
91 field_simp
92 ring
93
94theorem jq_nonneg {t : ℚ} (ht : 0 < t) : 0 ≤ jq t := by
95 rw [jq_closed (ne_of_gt ht)]
96 positivity
97
98theorem jq_lt_zero {t : ℚ} (ht : t < 0) : jq t < 0 := by
99 rw [jq_closed (ne_of_lt ht)]
100 apply div_neg_of_pos_of_neg
101 · exact pow_two_pos_of_ne_zero (by linarith)
102 · linarith
103
104/-- The unit is the only zero-cost orbit. -/
105theorem jq_eq_zero {t : ℚ} (ht : t ≠ 0) (h : jq t = 0) : t = 1 := by
106 rw [jq_closed ht] at h
107 rcases div_eq_zero_iff.mp h with h1 | h1
108 · have : t - 1 = 0 := by
109 have h2 : (t - 1) ^ 2 = 0 := h1
110 exact pow_eq_zero_iff (n := 2) (by norm_num) |>.mp h2
111 linarith
112 · exact absurd h1 (by simpa using ht)
113
114/-- Sign reversal on displays: reversing a distinction negates its doubled
115trace. -/
116theorem jq_neg (t : ℚ) : jq (-t) = -jq t - 2 := by
117 simp only [jq, inv_neg]
118 ring
119
120/-- `jq` is reciprocal-symmetric. -/
121theorem jq_inv (t : ℚ) : jq t⁻¹ = jq t := by
122 rcases eq_or_ne t 0 with h | h
123 · simp [h]
124 · unfold jq
125 rw [inv_inv]
126 ring
127
128theorem jq_mono {s t : ℚ} (hs : 1 ≤ s) (hst : s ≤ t) : jq s ≤ jq t := by
129 have hs0 : (0:ℚ) < s := lt_of_lt_of_le zero_lt_one hs
130 have ht0 : (0:ℚ) < t := lt_of_lt_of_le hs0 hst
131 have hkey : t + t⁻¹ - (s + s⁻¹) = (t - s) * (s * t - 1) / (s * t) := by
132 field_simp
133 ring
134 have hnum : 0 ≤ (t - s) * (s * t - 1) := by
135 apply mul_nonneg (by linarith)
136 nlinarith
137 have : 0 ≤ t + t⁻¹ - (s + s⁻¹) := by
138 rw [hkey]
139 exact div_nonneg hnum (by positivity)
140 unfold jq
141 linarith
142
143theorem jq_strictMono {s t : ℚ} (hs : 1 ≤ s) (hst : s < t) : jq s < jq t := by
144 have hs0 : (0:ℚ) < s := lt_of_lt_of_le zero_lt_one hs
145 have ht0 : (0:ℚ) < t := lt_trans hs0 hst
146 have hst1 : 1 < s * t := by nlinarith
147 have hkey : t + t⁻¹ - (s + s⁻¹) = (t - s) * (s * t - 1) / (s * t) := by
148 field_simp
149 ring
150 have hnum : 0 < (t - s) * (s * t - 1) := by
151 apply mul_pos (by linarith)
152 linarith
153 have : 0 < t + t⁻¹ - (s + s⁻¹) := by
154 rw [hkey]
155 exact div_pos hnum (by positivity)
156 unfold jq
157 linarith
158
159/-- Order reflection: on the region at or above the unit, `jq` sees the order. -/
160theorem jq_le_reflect {s t : ℚ} (_hs : 1 ≤ s) (ht : 1 ≤ t) (h : jq s ≤ jq t) :
161 s ≤ t := by
162 by_contra hc
163 push_neg at hc
164 exact absurd h (not_le.mpr (jq_strictMono ht hc))
165
166/-- The composition law, on displays. `jq` satisfies it for every nonzero pair,
167which is what makes the whole power family available to the gauge orbit. -/
168theorem jq_rcl {x y : ℚ} (hx : x ≠ 0) (hy : y ≠ 0) :
169 jq (x * y) + jq (x / y) = 2 * (jq x * jq y) + 2 * jq x + 2 * jq y := by
170 simp only [jq]
171 field_simp
172 ring
173
174/-- `jq` at a value strictly between the unit and `2` is below `jq 2`. -/
175
176theorem jq_two : jq 2 = 1 / 4 := by norm_num [jq]
177
178/-- The two solutions of `jq x = jq 2`. -/
179theorem jq_eq_two_cases {x : ℚ} (hx : x ≠ 0) (h : jq x = jq 2) :
180 x = 2 ∨ x = 2⁻¹ := by
181 rw [jq_two] at h
182 unfold jq at h
183 have h4 : 4 * (x + x⁻¹) - 8 = 2 := by
184 field_simp at h ⊢
185 linarith
186 have hquad : (x - 2) * (2 * x - 1) = 0 := by
187 have hxx : x * x⁻¹ = 1 := mul_inv_cancel₀ hx
188 field_simp at h4
189 nlinarith [h4, hxx]
190 rcases mul_eq_zero.mp hquad with h1 | h1
191 · left; linarith
192 · right
193 have : x = 1 / 2 := by linarith
194 rw [this]; norm_num
195
196/-! ## Part 1: positive integer orbits -/
197
198/-- The orbit whose display is the natural number `n`. -/
199def natOrbit (n : ℕ) : RatioOrbit := ratioOrbitOfRat (n : ℚ)
200
201@[simp] theorem natOrbit_toRat (n : ℕ) : (natOrbit n).toRat = (n : ℚ) :=
202 ratioOrbitOfRat_toRat _
203
204/-- An orbit displaying a positive integer. -/
205def IsPosIntOrbit (q : RatioOrbit) : Prop := ∃ n : ℕ, 1 ≤ n ∧ q.toRat = (n : ℚ)
206
207theorem natOrbit_isPosInt {n : ℕ} (hn : 1 ≤ n) : IsPosIntOrbit (natOrbit n) :=
208 ⟨n, hn, natOrbit_toRat n⟩
209
210theorem two_isPosInt : IsPosIntOrbit two := ⟨2, by norm_num, by simp [two_toRat]⟩
211
212theorem primeDirection_isPosInt {p : DistinctionNat}
213 (hp : DistinctionNat.primeOrbit p) : IsPosIntOrbit (primeDirection p hp) := by
214 refine ⟨p.toNat, ?_, by rw [primeDirection_toRat]⟩
215 have h := primeDirection_toRat_ne_zero p hp
216 rw [primeDirection_toRat] at h
217 exact Nat.one_le_iff_ne_zero.mpr (by exact_mod_cast h)
218
219/-! ## Part 2: the two structural axioms
220
221Neither mentions the canonical cost. The first says a cost read backwards is
222the negated cost (ledger antisymmetry); the second says a bigger imbalance
223costs at least as much. -/
224
225/-- **Sign reversal.** Reversing the orientation of a distinction negates its
226doubled trace: with `T = 2(F+1)`, this is `T(-q) = -T(q)`, written on displays
227as `F(-q) = -F(q) - 2`. -/
228def PRCNativeCostSignReversing (F : RatioOrbit → RatioOrbit) : Prop :=
229 ∀ q r : RatioOrbit, r.toRat = -q.toRat →
230 (F r).toRat = -(F q).toRat - 2
231
232/-- **Monotonicity.** On positive integer orbits, cost does not decrease as the
233imbalance grows. -/
234def PRCNativeCostMonotone (F : RatioOrbit → RatioOrbit) : Prop :=
235 ∀ a b : RatioOrbit, IsPosIntOrbit a → IsPosIntOrbit b →
236 a.toRat ≤ b.toRat → (F a).toRat ≤ (F b).toRat
237
238/-- **Positivity.** Recognizing a difference never pays; this is DERIVED below,
239not assumed. -/
240def PRCNativeCostPositive (F : RatioOrbit → RatioOrbit) : Prop :=
241 ∀ q : RatioOrbit, 0 < q.toRat → 0 ≤ (F q).toRat
242
243/-! ## Part 3: the canonical cost satisfies both structural axioms -/
244
245theorem canonicalSelectedNativeCost_jq (q : RatioOrbit) :
246 (canonicalSelectedNativeCost q).toRat = jq q.toRat :=
247 canonicalSelectedNativeCost_toRat q
248
249theorem canonicalSelectedNativeCost_signReversing :
250 PRCNativeCostSignReversing canonicalSelectedNativeCost := by
251 intro q r hr
252 rw [canonicalSelectedNativeCost_jq, canonicalSelectedNativeCost_jq, hr]
253 rcases eq_or_ne q.toRat 0 with h | h
254 · rw [h]
255 norm_num
256 · simp only [jq, inv_neg]
257 ring
258
259theorem canonicalSelectedNativeCost_monotone :
260 PRCNativeCostMonotone canonicalSelectedNativeCost := by
261 rintro a b ⟨m, hm, ham⟩ ⟨n, hn, hbn⟩ hab
262 rw [canonicalSelectedNativeCost_jq, canonicalSelectedNativeCost_jq]
263 apply jq_mono
264 · rw [ham]; exact_mod_cast hm
265 · exact hab
266
267theorem canonicalSelectedNativeCost_positive :
268 PRCNativeCostPositive canonicalSelectedNativeCost := by
269 intro q hq
270 rw [canonicalSelectedNativeCost_jq]
271 exact jq_nonneg hq
272
273/-! ## Part 4 (ROUND 4): sign reversal derives the signed-unit calibration -/
274
275/-- **The signed-unit field is not an assumption.** Ledger antisymmetry applied
276at the unit produces it. -/
277theorem signReversing_forces_signed_unit {F : RatioOrbit → RatioOrbit}
278 (hunit : F RatioOrbit.one = RatioOrbit.zero)
279 (hsign : PRCNativeCostSignReversing F) :
280 PRCNativeCostSignedUnitCalibrated F := by
281 have hneg : negativeOneRatio.toRat = -(RatioOrbit.one.toRat) := by
282 rw [negativeOneRatio_toRat, RatioOrbit.one_toRat]
283 have h := hsign RatioOrbit.one negativeOneRatio hneg
284 rw [PRCNativeCostSignedUnitCalibrated, RatioOrbit.crossEq_iff_toRat_eq,
285 jq_onRatioOrbit, negativeOneRatio_toRat, h, hunit, RatioOrbit.zero_toRat]
286 norm_num [jq]
287
288/-- The round-4 class: base plus prime pairs plus SIGN REVERSAL plus the zero
289orbit. Compared with the round-2 slim ledger, the signed-unit calibration is
290gone and an intrinsic antisymmetry axiom stands in its place. -/
291structure PRCSignReversingNativeCostHypotheses
292 (F : RatioOrbit → RatioOrbit) : Prop where
293 strengthened : PRCStrengthenedNativeCostHypotheses F
294 sign_reversing : PRCNativeCostSignReversing F
295 zero_calibrated : PRCDoubledTraceZeroCalibrated (nativeCostDoubledTrace F)
296
297def PRCSignReversingNativeCostUniquenessTarget : Prop :=
298 ∀ F : RatioOrbit → RatioOrbit,
299 PRCSignReversingNativeCostHypotheses F →
300 ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (onRatioOrbit q)
301
302/-- Round 4 terminal: the sign-reversing ledger forces the canonical cost. -/
303theorem PRCSignReversingNativeCostUniquenessTarget_proved :
304 PRCSignReversingNativeCostUniquenessTarget := by
305 intro F hF q
306 refine PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved F ?_ q
307 exact
308 { signed_strengthened :=
309 { strengthened := hF.strengthened
310 signed_unit :=
311 signReversing_forces_signed_unit
312 hF.strengthened.native.unit_zero hF.sign_reversing }
313 zero_calibrated := hF.zero_calibrated }
314
315/-- Non-vacuity of the round-4 class. -/
316theorem canonicalSelectedNativeCost_signReversing_hypotheses :
317 PRCSignReversingNativeCostHypotheses canonicalSelectedNativeCost :=
318 { strengthened :=
319 canonicalSelectedNativeCost_slim_hypotheses.signed_strengthened.strengthened
320 sign_reversing := canonicalSelectedNativeCost_signReversing
321 zero_calibrated := canonicalSelectedNativeCost_slim_hypotheses.zero_calibrated }
322
323/-- The exchange is real in both directions: the round-4 class and the round-2
324slim ledger carve out the same costs. Sign reversal is therefore a strictly
325better-behaved stand-in for the signed-unit calibration, not a weakening. -/
326theorem signReversing_class_forces_slim (F : RatioOrbit → RatioOrbit)
327 (hF : PRCSignReversingNativeCostHypotheses F) :
328 PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses F :=
329 { signed_strengthened :=
330 { strengthened := hF.strengthened
331 signed_unit :=
332 signReversing_forces_signed_unit
333 hF.strengthened.native.unit_zero hF.sign_reversing }
334 zero_calibrated := hF.zero_calibrated }
335
336/-- The absolute-value cost is the round-3 witness that the signed-unit field
337was load bearing; it is excluded by sign reversal directly, with no reference
338to the canonical cost's value anywhere. -/
339theorem absValueGeneratedNativeCost_not_signReversing :
340 ¬ PRCNativeCostSignReversing absValueGeneratedNativeCost := by
341 intro h
342 have hneg : negativeOneRatio.toRat = -(RatioOrbit.one.toRat) := by
343 rw [negativeOneRatio_toRat, RatioOrbit.one_toRat]
344 have hval := h RatioOrbit.one negativeOneRatio hneg
345 have hone : (absValueGeneratedNativeCost RatioOrbit.one).toRat = 0 := by
346 unfold absValueGeneratedNativeCost
347 simp
348 have hminus : (absValueGeneratedNativeCost negativeOneRatio).toRat = 0 := by
349 have := absValueGeneratedNativeCost_negative_one_zero
350 rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.zero_toRat] at this
351 exact this
352 rw [hminus, hone] at hval
353 norm_num at hval
354
355/-! ## Part 5: the squeeze
356
357Erdős's 1946 monotonicity rigidity, in the completely multiplicative case,
358written with no logarithm and no real number. The content is that a positive
359rational is determined by where its powers fall among the powers of a fixed
360base: two rationals with the same cut are equal. -/
361
362/-- Archimedean growth for rational powers, from Bernoulli's inequality. -/
363private lemma exists_pow_gt_rat {b : ℚ} (hb : 1 < b) (c : ℚ) :
364 ∃ n : ℕ, c < b ^ n := by
365 obtain ⟨n, hn⟩ := exists_nat_gt ((c - 1) / (b - 1))
366 refine ⟨n, ?_⟩
367 have hb1 : (0:ℚ) < b - 1 := by linarith
368 have hbern : 1 + (n : ℚ) * (b - 1) ≤ (1 + (b - 1)) ^ n :=
369 one_add_mul_le_pow (by linarith) n
370 have hlt : c - 1 < (n : ℚ) * (b - 1) := by
371 rw [div_lt_iff₀ hb1] at hn
372 exact hn
373 have hsimp : (1 : ℚ) + (b - 1) = b := by ring
374 rw [hsimp] at hbern
375 linarith
376
377/-- One side of the cut squeeze. -/
378private lemma cut_pins_aux {u v α γ γ' : ℚ}
379 (hα : 1 < α) (hγ : 1 ≤ γ) (hlt : γ < γ')
380 (hf : ∀ m n : ℕ, u ^ m ≤ v ^ n → α ^ m ≤ γ ^ n)
381 (hb' : ∀ m n : ℕ, v ^ n ≤ u ^ m → γ' ^ n ≤ α ^ m) :
382 False := by
383 classical
384 have hγ0 : (0:ℚ) < γ := lt_of_lt_of_le zero_lt_one hγ
385 have hα0 : (0:ℚ) < α := lt_trans zero_lt_one hα
386 have hratio : 1 < γ' / γ := (one_lt_div hγ0).mpr hlt
387 obtain ⟨n, hn⟩ := exists_pow_gt_rat hratio α
388 have hγn : (0:ℚ) < γ ^ n := pow_pos hγ0 n
389 have hkey : α * γ ^ n < γ' ^ n := by
390 rw [div_pow, lt_div_iff₀ hγn] at hn
391 linarith
392 have hex : ∃ m : ℕ, γ ^ n < α ^ m := exists_pow_gt_rat hα (γ ^ n)
393 set m := Nat.find hex with hmdef
394 have hmspec : γ ^ n < α ^ m := Nat.find_spec hex
395 have hm0 : m ≠ 0 := by
396 intro h0
397 rw [h0, pow_zero] at hmspec
398 exact absurd (one_le_pow₀ hγ) (not_le.mpr hmspec)
399 obtain ⟨j, hj⟩ := Nat.exists_eq_succ_of_ne_zero hm0
400 have hmin : ¬ (γ ^ n < α ^ j) := Nat.find_min hex (by omega)
401 push_neg at hmin
402 have hαm : α ^ m ≤ α * γ ^ n := by
403 calc α ^ m = α ^ j * α := by rw [hj, pow_succ]
404 _ ≤ γ ^ n * α := mul_le_mul_of_nonneg_right hmin (le_of_lt hα0)
405 _ = α * γ ^ n := by ring
406 have hlt2 : α ^ m < γ' ^ n := lt_of_le_of_lt hαm hkey
407 rcases le_total (u ^ m) (v ^ n) with h | h
408 · exact absurd (hf m n h) (not_le.mpr hmspec)
409 · exact absurd (hb' m n h) (not_le.mpr hlt2)
410
411/-- **The cut lemma.** Two rationals at or above the unit that transport the
412same integer-exponent comparisons against a common reference cut are equal.
413This is the whole of the Erdős squeeze, and there is no analysis in it. -/
414theorem cut_pins {u v α γ γ' : ℚ}
415 (hα : 1 < α) (hγ : 1 ≤ γ) (hγ' : 1 ≤ γ')
416 (hf : ∀ m n : ℕ, u ^ m ≤ v ^ n → α ^ m ≤ γ ^ n)
417 (hb : ∀ m n : ℕ, v ^ n ≤ u ^ m → γ ^ n ≤ α ^ m)
418 (hf' : ∀ m n : ℕ, u ^ m ≤ v ^ n → α ^ m ≤ γ' ^ n)
419 (hb' : ∀ m n : ℕ, v ^ n ≤ u ^ m → γ' ^ n ≤ α ^ m) :
420 γ = γ' := by
421 rcases lt_trichotomy γ γ' with h | h | h
422 · exact (cut_pins_aux hα hγ h hf hb').elim
423 · exact h
424 · exact (cut_pins_aux hα hγ' h hf' hb).elim
425
426/-- The arithmetic data a monotone character leaves on the positive integers:
427completely multiplicative, nowhere zero, with nondecreasing cost. -/
428structure MonoMult (h : ℕ → ℚ) : Prop where
429 ne : ∀ n : ℕ, 1 ≤ n → h n ≠ 0
430 one : h 1 = 1
431 mul : ∀ m n : ℕ, 1 ≤ m → 1 ≤ n → h (m * n) = h m * h n
432 mono : ∀ m n : ℕ, 1 ≤ m → m ≤ n → jq (h m) ≤ jq (h n)
433
434namespace MonoMult
435
436theorem pow {h : ℕ → ℚ} (H : MonoMult h) (a k : ℕ) (ha : 1 ≤ a) :
437 h (a ^ k) = (h a) ^ k := by
438 induction k with
439 | zero => simpa using H.one
440 | succ k ih =>
441 have h1 : 1 ≤ a ^ k := Nat.one_le_pow _ _ ha
442 rw [pow_succ, H.mul _ _ h1 ha, ih, pow_succ]
443
444/-- Monotonicity alone rules out negative values above the unit. -/
445theorem pos {h : ℕ → ℚ} (H : MonoMult h) (hα : 0 < h 2) :
446 ∀ n : ℕ, 2 ≤ n → 0 < h n := by
447 intro n hn
448 rcases lt_trichotomy (h n) 0 with hlt | heq | hgt
449 · exfalso
450 have hmm := H.mono 2 n (by norm_num) hn
451 have h1 := jq_lt_zero hlt
452 have h2 := jq_nonneg hα
453 linarith
454 · exact absurd heq (H.ne n (by omega))
455 · exact hgt
456
457/-- A monotone character whose anchor exceeds the unit exceeds it everywhere
458above the unit. Interpolating an anchor power into the dip is the contradiction:
459if some value fell below the unit, some larger integer would cost less than
460`2` does. -/
461theorem ge_one {h : ℕ → ℚ} (H : MonoMult h) (hα : 1 < h 2) :
462 ∀ n : ℕ, 2 ≤ n → 1 ≤ h n := by
463 classical
464 intro n hn
465 by_contra hc
466 push_neg at hc
467 have hα0 : (0:ℚ) < h 2 := lt_trans zero_lt_one hα
468 have hn0 : 0 < h n := H.pos hα0 n hn
469 have hex : ∃ k : ℕ, (1:ℚ) ≤ (h 2) ^ k * h n := by
470 obtain ⟨k, hk⟩ := exists_pow_gt_rat hα ((h n)⁻¹)
471 refine ⟨k, ?_⟩
472 have hmul' := mul_lt_mul_of_pos_right hk hn0
473 rw [inv_mul_cancel₀ (ne_of_gt hn0)] at hmul'
474 exact le_of_lt hmul'
475 set k := Nat.find hex with hkdef
476 have hkspec : (1:ℚ) ≤ (h 2) ^ k * h n := Nat.find_spec hex
477 have hk0 : k ≠ 0 := by
478 intro h0
479 rw [h0, pow_zero, one_mul] at hkspec
480 linarith
481 obtain ⟨j, hj⟩ := Nat.exists_eq_succ_of_ne_zero hk0
482 have hmin : ¬ ((1:ℚ) ≤ (h 2) ^ j * h n) := Nat.find_min hex (by omega)
483 push_neg at hmin
484 have hupper : (h 2) ^ k * h n < h 2 := by
485 have hrw : (h 2) ^ k * h n = h 2 * ((h 2) ^ j * h n) := by
486 rw [hj, pow_succ]; ring
487 have hstep := mul_lt_mul_of_pos_left hmin hα0
488 rw [hrw, mul_one] at *
489 linarith
490 have hval : h (2 ^ k * n) = (h 2) ^ k * h n := by
491 rw [H.mul _ _ (Nat.one_le_pow _ _ (by norm_num)) (by omega),
492 H.pow 2 k (by norm_num)]
493 have hbig : 2 ≤ 2 ^ k * n := by
494 have h2k : 2 ^ 1 ≤ 2 ^ k := Nat.pow_le_pow_right (by norm_num) (by omega)
495 have : 2 * 1 ≤ 2 ^ k * n := Nat.mul_le_mul (by simpa using h2k) (by omega)
496 simpa using this
497 have hmm := H.mono 2 (2 ^ k * n) (by norm_num) hbig
498 rw [hval] at hmm
499 have hstrict := jq_strictMono hkspec hupper
500 linarith
501
502theorem transfer_le {h : ℕ → ℚ} (H : MonoMult h) (hα : 1 < h 2)
503 {n : ℕ} (hn : 2 ≤ n) (m k : ℕ) (hmk : (2:ℚ) ^ m ≤ (n : ℚ) ^ k) :
504 (h 2) ^ m ≤ (h n) ^ k := by
505 have hnat : 2 ^ m ≤ n ^ k := by exact_mod_cast hmk
506 have hmm := H.mono (2 ^ m) (n ^ k) (Nat.one_le_pow _ _ (by norm_num)) hnat
507 rw [H.pow 2 m (by norm_num), H.pow n k (by omega)] at hmm
508 exact jq_le_reflect (one_le_pow₀ (le_of_lt hα))
509 (one_le_pow₀ (H.ge_one hα n hn)) hmm
510
511theorem transfer_ge {h : ℕ → ℚ} (H : MonoMult h) (hα : 1 < h 2)
512 {n : ℕ} (hn : 2 ≤ n) (m k : ℕ) (hmk : (n : ℚ) ^ k ≤ (2:ℚ) ^ m) :
513 (h n) ^ k ≤ (h 2) ^ m := by
514 have hnat : n ^ k ≤ 2 ^ m := by exact_mod_cast hmk
515 have hmm := H.mono (n ^ k) (2 ^ m) (Nat.one_le_pow _ _ (by omega)) hnat
516 rw [H.pow 2 m (by norm_num), H.pow n k (by omega)] at hmm
517 exact jq_le_reflect (one_le_pow₀ (H.ge_one hα n hn))
518 (one_le_pow₀ (le_of_lt hα)) hmm
519
520/-- The degenerate gauge member: anchoring at the unit collapses the whole
521cost. This is the sign character, the `c = 0` member of the power family. -/
522theorem trivial_of_two_eq_one {h : ℕ → ℚ} (H : MonoMult h) (hα : h 2 = 1) :
523 ∀ n : ℕ, 1 ≤ n → h n = 1 := by
524 have hpow2 : ∀ n : ℕ, n ≤ 2 ^ n := by
525 intro n
526 induction n with
527 | zero => norm_num
528 | succ k ih =>
529 have h1 : 1 ≤ 2 ^ k := Nat.one_le_two_pow
530 have : 2 ^ (k + 1) = 2 ^ k * 2 := by rw [pow_succ]
531 omega
532 intro n hn
533 rcases Nat.lt_or_ge n 2 with h2 | h2
534 · have hn1 : n = 1 := by omega
535 rw [hn1, H.one]
536 · have hlow := H.mono 2 n (by norm_num) h2
537 rw [hα, jq_one] at hlow
538 have hup := H.mono n (2 ^ n) (by omega) (hpow2 n)
539 rw [H.pow 2 n (by norm_num), hα, one_pow, jq_one] at hup
540 exact jq_eq_zero (H.ne n hn) (le_antisymm hup hlow)
541
542end MonoMult
543
544/-- **The gauge theorem (Erdős 1946, completely multiplicative case).** Two
545monotone characters that agree at the single index `2` agree at every positive
546index. No logarithm, no limit, no real number: the anchor value fixes the whole
547arithmetic function through the cut squeeze. -/
548theorem monoMult_gauge {h₁ h₂ : ℕ → ℚ} (H₁ : MonoMult h₁) (H₂ : MonoMult h₂)
549 (hanchor : h₁ 2 = h₂ 2) (hα : 1 ≤ h₁ 2) :
550 ∀ n : ℕ, 1 ≤ n → h₁ n = h₂ n := by
551 rcases eq_or_lt_of_le hα with heq | hlt
552 · intro n hn
553 rw [H₁.trivial_of_two_eq_one heq.symm n hn,
554 H₂.trivial_of_two_eq_one (by rw [← hanchor]; exact heq.symm) n hn]
555 · intro n hn
556 rcases Nat.lt_or_ge n 2 with h2 | h2
557 · have hn1 : n = 1 := by omega
558 rw [hn1, H₁.one, H₂.one]
559 · have hlt2 : 1 < h₂ 2 := by rw [← hanchor]; exact hlt
560 refine cut_pins hlt (H₁.ge_one hlt n h2) (H₂.ge_one hlt2 n h2)
561 (H₁.transfer_le hlt h2) (H₁.transfer_ge hlt h2) ?_ ?_
562 · intro m k hmk
563 rw [hanchor]
564 exact H₂.transfer_le hlt2 h2 m k hmk
565 · intro m k hmk
566 rw [hanchor]
567 exact H₂.transfer_ge hlt2 h2 m k hmk
568
569theorem natCast_monoMult : MonoMult (fun n : ℕ => (n : ℚ)) where
570 ne := fun n hn => by
571 exact_mod_cast Nat.one_le_iff_ne_zero.mp hn
572 one := by norm_num
573 mul := fun m n _ _ => by push_cast; ring
574 mono := fun m n hm hmn => by
575 exact jq_mono (by exact_mod_cast hm) (by exact_mod_cast hmn)
576
577/-- **Monotone rigidity.** A monotone character sending `2` to `2` is the
578identity on the positive integers. The round-5 engine, and the special case of
579the gauge theorem in which the second character is the identity. -/
580theorem monotone_multiplicative_pins {h : ℕ → ℚ} (H : MonoMult h)
581 (htwo : h 2 = 2) :
582 ∀ n : ℕ, 1 ≤ n → h n = (n : ℚ) :=
583 monoMult_gauge H natCast_monoMult (by rw [htwo]; norm_num)
584 (by rw [htwo]; norm_num)
585
586/-! ## Part 6 (ROUND 5): the structural ledger forces the canonical cost -/
587
588/-- **The structural ledger.** Base (reciprocity, normalization invariance, the
589nonzero composition law, unit-zero, and the single orbit-2 anchor) plus SIGN
590REVERSAL plus MONOTONICITY plus the zero-orbit convention. Compared with the
591round-2 slim ledger, the countable prime-pair product family and the signed-unit
592calibration are both gone; nothing that replaced them mentions the canonical
593cost. -/
594structure PRCStructuralNativeCostHypotheses
595 (F : RatioOrbit → RatioOrbit) : Prop where
596 native : PRCNativeCostHypotheses F
597 sign_reversing : PRCNativeCostSignReversing F
598 monotone : PRCNativeCostMonotone F
599 zero_calibrated : PRCDoubledTraceZeroCalibrated (nativeCostDoubledTrace F)
600
601def PRCStructuralNativeCostUniquenessTarget : Prop :=
602 ∀ F : RatioOrbit → RatioOrbit,
603 PRCStructuralNativeCostHypotheses F →
604 ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (onRatioOrbit q)
605
606/-- The character attached to a structural cost is the identity in display on
607every positive integer orbit, up to the global reciprocal orientation that the
608cost cannot see. This is the round-5 engine. -/
609theorem structural_character_calibrated_on_positive_integers
610 {F χ : RatioOrbit → RatioOrbit}
611 (hF : PRCStructuralNativeCostHypotheses F)
612 (hχ : PRCRatioCharacter χ)
613 (hFχ : ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (costFromCharacter χ q)) :
614 ∀ n : ℕ, 1 ≤ n → jq ((χ (natOrbit n)).toRat) = jq ((n : ℚ)) := by
615 classical
616 have hresp : PRCCharacterRespectsCrossEq χ :=
617 PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical hχ
618 PRCNormalizeRatioCanonicalTarget_proved
619 have hchi : ∀ a b : RatioOrbit, a.toRat = b.toRat →
620 (χ a).toRat = (χ b).toRat := by
621 intro a b hab
622 exact crossDisp
623 (hresp a b (dispCross hab))
624 set g : ℕ → ℚ := fun n => (χ (natOrbit n)).toRat with hgdef
625 -- the cost display of F at any orbit
626 have hFdisp : ∀ q : RatioOrbit, (F q).toRat = jq ((χ q).toRat) := by
627 intro q
628 rw [crossDisp (hFχ q), costFromCharacter_jq]
629 have hone : g 1 = 1 := by
630 have h1 : (natOrbit 1).toRat = RatioOrbit.one.toRat := by
631 rw [natOrbit_toRat, RatioOrbit.one_toRat]; norm_num
632 have h2 := hchi _ _ h1
633 show (χ (natOrbit 1)).toRat = 1
634 rw [h2, crossDisp hχ.unit, RatioOrbit.one_toRat]
635 have hmulg : ∀ m n : ℕ, 1 ≤ m → 1 ≤ n → g (m * n) = g m * g n := by
636 intro m n _ _
637 have hdisp : (natOrbit (m * n)).toRat =
638 (RatioOrbit.mul (natOrbit m) (natOrbit n)).toRat := by
639 rw [natOrbit_toRat, RatioOrbit.mul_toRat, natOrbit_toRat, natOrbit_toRat]
640 push_cast
641 ring
642 have h1 := hchi _ _ hdisp
643 have h2 := crossDisp
644 (hχ.multiplicative (natOrbit m) (natOrbit n))
645 show (χ (natOrbit (m * n))).toRat
646 = (χ (natOrbit m)).toRat * (χ (natOrbit n)).toRat
647 rw [h1, h2, RatioOrbit.mul_toRat]
648 have hne : ∀ n : ℕ, 1 ≤ n → g n ≠ 0 := by
649 intro n hn
650 refine hχ.nonzero_preserving ?_
651 rw [natOrbit_toRat]
652 exact_mod_cast Nat.one_le_iff_ne_zero.mp hn
653 have hmonog : ∀ m n : ℕ, 1 ≤ m → m ≤ n → jq (g m) ≤ jq (g n) := by
654 intro m n hm hmn
655 have := hF.monotone (natOrbit m) (natOrbit n) (natOrbit_isPosInt hm)
656 (natOrbit_isPosInt (le_trans hm hmn)) (by
657 rw [natOrbit_toRat, natOrbit_toRat]; exact_mod_cast hmn)
658 rw [hFdisp, hFdisp] at this
659 exact this
660 have hg2 : g 2 = 2 ∨ g 2 = 2⁻¹ := by
661 have hdisp : (natOrbit 2).toRat = two.toRat := by
662 rw [natOrbit_toRat, two_toRat]; norm_num
663 have hval : jq (g 2) = jq 2 := by
664 have hcal := crossDisp hF.native.two_calibrated
665 rw [hFdisp, jq_onRatioOrbit, two_toRat] at hcal
666 show jq ((χ (natOrbit 2)).toRat) = jq 2
667 rw [hchi _ _ hdisp]
668 exact hcal
669 exact jq_eq_two_cases (hne 2 (by norm_num)) hval
670 have Hg : MonoMult g := ⟨hne, hone, hmulg, hmonog⟩
671 have Hginv : MonoMult (fun k => (g k)⁻¹) :=
672 { ne := fun k hk => inv_ne_zero (hne k hk)
673 one := by rw [hone]; norm_num
674 mul := fun a b ha hb => by rw [hmulg a b ha hb, mul_inv]
675 mono := fun a b ha hab => by
676 rw [jq_inv, jq_inv]
677 exact hmonog a b ha hab }
678 intro n hn
679 show jq (g n) = jq ((n : ℚ))
680 rcases hg2 with h2 | h2
681 · rw [monotone_multiplicative_pins Hg h2 n hn]
682 · have hinvtwo : (fun k => (g k)⁻¹) 2 = 2 := by show (g 2)⁻¹ = 2; rw [h2]; norm_num
683 have hres := monotone_multiplicative_pins Hginv hinvtwo n hn
684 calc jq (g n) = jq ((g n)⁻¹) := (jq_inv (g n)).symm
685 _ = jq ((n : ℚ)) := by rw [hres]
686
687/-- **Round 5 terminal.** The structural ledger forces the canonical cost. -/
688theorem PRCStructuralNativeCostUniquenessTarget_proved :
689 PRCStructuralNativeCostUniquenessTarget := by
690 intro F hF q
691 obtain ⟨χ, hχ, hFχ⟩ :=
692 PRCZeroCalibratedNativeCostCharacterFactorizationTarget_proved F hF.native
693 hF.zero_calibrated
694 have hcal := structural_character_calibrated_on_positive_integers hF hχ hFχ
695 have hresp : PRCCharacterRespectsCrossEq χ :=
696 PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical hχ
697 PRCNormalizeRatioCanonicalTarget_proved
698 have hchi : ∀ a b : RatioOrbit, a.toRat = b.toRat →
699 (χ a).toRat = (χ b).toRat := by
700 intro a b hab
701 exact crossDisp
702 (hresp a b (dispCross hab))
703 -- every positive integer orbit is calibrated
704 have hposcal : ∀ (a : RatioOrbit), IsPosIntOrbit a →
705 RatioOrbit.crossEq (costFromCharacter χ a) (onRatioOrbit a) := by
706 rintro a ⟨n, hn, han⟩
707 have hdisp : a.toRat = (natOrbit n).toRat := by rw [natOrbit_toRat, han]
708 rw [RatioOrbit.crossEq_iff_toRat_eq, costFromCharacter_jq, jq_onRatioOrbit,
709 han]
710 have hn' := hcal n hn
711 rw [← hchi a (natOrbit n) hdisp] at hn'
712 exact hn'
713 have hprime : PRCCharacterPrimeDirectionCalibrated χ := fun p hp =>
714 hposcal _ (primeDirection_isPosInt hp)
715 have hpair : PRCCharacterPrimePairProductCostConsistent χ := by
716 intro p hp r hr
717 refine hposcal _ ⟨p.toNat * r.toNat, ?_, ?_⟩
718 · obtain ⟨a, ha, _⟩ := primeDirection_isPosInt hp
719 obtain ⟨b, hb, _⟩ := primeDirection_isPosInt hr
720 have hpn : 1 ≤ p.toNat := by
721 have h := primeDirection_toRat_ne_zero p hp
722 rw [primeDirection_toRat] at h
723 exact Nat.one_le_iff_ne_zero.mpr (by exact_mod_cast h)
724 have hrn : 1 ≤ r.toNat := by
725 have h := primeDirection_toRat_ne_zero r hr
726 rw [primeDirection_toRat] at h
727 exact Nat.one_le_iff_ne_zero.mpr (by exact_mod_cast h)
728 exact Nat.one_le_iff_ne_zero.mpr (Nat.mul_ne_zero (by omega) (by omega))
729 · rw [RatioOrbit.mul_toRat, primeDirection_toRat, primeDirection_toRat]
730 push_cast
731 ring
732 have hsignCost :
733 RatioOrbit.crossEq (costFromCharacter χ negativeOneRatio)
734 (onRatioOrbit negativeOneRatio) :=
735 RatioOrbit.crossEq_trans (RatioOrbit.crossEq_symm (hFχ negativeOneRatio))
736 (signReversing_forces_signed_unit hF.native.unit_zero hF.sign_reversing)
737 have hsign : PRCCharacterSignedUnitCalibrated χ :=
738 costFromCharacter_negativeOne_forces_signed_unit hχ hsignCost
739 exact RatioOrbit.crossEq_trans (hFχ q)
740 (PRCNativeCostSignedAdmissibleCharacterRigidityTarget_proved χ
741 ⟨⟨hχ, hprime, hpair⟩, hsign⟩ q)
742
743/-- Non-vacuity of the structural ledger. -/
744theorem canonicalSelectedNativeCost_structural_hypotheses :
745 PRCStructuralNativeCostHypotheses canonicalSelectedNativeCost :=
746 { native :=
747 canonicalSelectedNativeCost_slim_hypotheses.signed_strengthened.strengthened.native
748 sign_reversing := canonicalSelectedNativeCost_signReversing
749 monotone := canonicalSelectedNativeCost_monotone
750 zero_calibrated := canonicalSelectedNativeCost_slim_hypotheses.zero_calibrated }
751
752/-- **The prime-pair product family is redundant against monotonicity.** Every
753inhabitant of the structural ledger satisfies it, and the whole round-1 and
754round-2 ledger besides. -/
755theorem structural_forces_slim (F : RatioOrbit → RatioOrbit)
756 (hF : PRCStructuralNativeCostHypotheses F) :
757 PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses F := by
758 have hJ := PRCStructuralNativeCostUniquenessTarget_proved F hF
759 exact
760 { signed_strengthened :=
761 { strengthened :=
762 { native := hF.native
763 prime_pair_product_cost := fun p hp r hr => hJ _ }
764 signed_unit :=
765 signReversing_forces_signed_unit hF.native.unit_zero hF.sign_reversing }
766 zero_calibrated := hF.zero_calibrated }
767
768/-- **Positivity is a theorem, not an axiom.** Recognizing a positive imbalance
769never pays. -/
770theorem structural_forces_positive (F : RatioOrbit → RatioOrbit)
771 (hF : PRCStructuralNativeCostHypotheses F) :
772 PRCNativeCostPositive F := by
773 intro q hq
774 have hJ := crossDisp
775 (PRCStructuralNativeCostUniquenessTarget_proved F hF q)
776 rw [hJ, jq_onRatioOrbit]
777 exact jq_nonneg hq
778
779/-! ## Part 7 (ROUND 6): the surviving anchor is a unit gauge
780
781Two claims, and together they are the free-side stratification. The gauge orbit
782is genuinely inhabited, so the anchor is a real choice and not a redundancy;
783and the anchor value determines everything else, so it is the ONLY choice. -/
784
785/-- The structural ledger with the anchor removed. -/
786structure PRCStructuralNativeCostHypothesesSansAnchor
787 (F : RatioOrbit → RatioOrbit) : Prop where
788 base_sans_two : PRCNativeCostHypothesesSansTwoCalibration F
789 sign_reversing : PRCNativeCostSignReversing F
790 monotone : PRCNativeCostMonotone F
791 zero_calibrated : PRCDoubledTraceZeroCalibrated (nativeCostDoubledTrace F)
792
793def PRCStructuralSansAnchorUniquenessTarget : Prop :=
794 ∀ F : RatioOrbit → RatioOrbit,
795 PRCStructuralNativeCostHypothesesSansAnchor F →
796 ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (onRatioOrbit q)
797
798/-- The structural ledger is exactly the anchor-free ledger plus the anchor, so
799what follows is a statement about the structural ledger's own last field. -/
800theorem structural_iff_sansAnchor_and_two_calibrated
801 (F : RatioOrbit → RatioOrbit) :
802 PRCStructuralNativeCostHypotheses F ↔
803 (PRCStructuralNativeCostHypothesesSansAnchor F ∧
804 RatioOrbit.crossEq (F two) (onRatioOrbit two)) := by
805 constructor
806 · intro h
807 exact ⟨⟨⟨h.native.reciprocal, h.native.normalized_invariant,
808 h.native.canonical_rcl, h.native.unit_zero⟩,
809 h.sign_reversing, h.monotone, h.zero_calibrated⟩,
810 h.native.two_calibrated⟩
811 · rintro ⟨h, htwo⟩
812 exact ⟨⟨h.base_sans_two.reciprocal, h.base_sans_two.normalized_invariant,
813 h.base_sans_two.canonical_rcl, h.base_sans_two.unit_zero, htwo⟩,
814 h.sign_reversing, h.monotone, h.zero_calibrated⟩
815
816/-! ### The odd power family inhabits the gauge orbit
817
818The round-3 impostors do not survive here: the Liouville twist and the two-adic
819twist are both non-monotone, which is exactly why monotonicity could replace the
820pair family. What is left is the ODD power family `q ↦ q^(2k+1)`, whose members
821are multiplicative, orientation-reversing, and monotone. The exponent must be
822odd: an even power destroys sign reversal, since it cannot tell `-q` from `q`.
823
824Every member of the family inhabits the anchor-free ledger, and distinct members
825disagree at the anchor. So the gauge orbit is not just nonempty, it is infinite,
826and the anchor is what picks one point of it. This is the free-side statement of
827"the form is forced, the unit is a choice": the choice is a discrete
828one-parameter family and the anchor is the coordinate on it. -/
829
830/-- The cost generated by the power `q ↦ q^n`. Stated for every exponent, not
831just the odd ones, because the parity is exactly what decides membership: every
832field below holds for all `n ≥ 1`, and sign reversal is the one that splits. -/
833def powerGeneratedNativeCost (n : ℕ) (q : RatioOrbit) : RatioOrbit :=
834 if q.toRat = 1 then RatioOrbit.zero
835 else onRatioOrbit (ratioOrbitOfRat (q.toRat ^ n))
836
837theorem powerGeneratedNativeCost_toRat (n : ℕ) (q : RatioOrbit) :
838 (powerGeneratedNativeCost n q).toRat = jq (q.toRat ^ n) := by
839 rw [powerGeneratedNativeCost]
840 by_cases h : q.toRat = 1
841 · rw [if_pos h, RatioOrbit.zero_toRat, h, one_pow]
842 norm_num [jq]
843 · rw [if_neg h, jq_onRatioOrbit, ratioOrbitOfRat_toRat]
844
845theorem powerGeneratedNativeCost_base (n : ℕ) :
846 PRCNativeCostHypothesesSansTwoCalibration (powerGeneratedNativeCost n) where
847 reciprocal := by
848 intro q
849 rw [RatioOrbit.crossEq_iff_toRat_eq, powerGeneratedNativeCost_toRat,
850 powerGeneratedNativeCost_toRat, RatioOrbit.recip_toRat, inv_pow, jq_inv]
851 normalized_invariant := by
852 intro q
853 rw [RatioOrbit.crossEq_iff_toRat_eq, powerGeneratedNativeCost_toRat,
854 powerGeneratedNativeCost_toRat, DistinctionNat.normalizeRatio_toRat]
855 canonical_rcl := by
856 intro x y hx hy
857 rw [RatioOrbit.crossEq_iff_toRat_eq]
858 simp only [RatioOrbit.add_toRat, RatioOrbit.mul_toRat,
859 powerGeneratedNativeCost_toRat, div_toRat, two_toRat]
860 rw [mul_pow, div_pow]
861 exact jq_rcl (pow_ne_zero _ hx) (pow_ne_zero _ hy)
862 unit_zero := by
863 rw [powerGeneratedNativeCost, if_pos RatioOrbit.one_toRat]
864
865theorem powerGeneratedNativeCost_monotone (n : ℕ) :
866 PRCNativeCostMonotone (powerGeneratedNativeCost n) := by
867 rintro a b ⟨m, hm, ham⟩ ⟨_, _, _⟩ hab
868 rw [powerGeneratedNativeCost_toRat, powerGeneratedNativeCost_toRat]
869 have ha1 : (1:ℚ) ≤ a.toRat := by rw [ham]; exact_mod_cast hm
870 refine jq_mono (one_le_pow₀ ha1) ?_
871 exact pow_le_pow_left₀ (le_trans zero_le_one ha1) hab _
872
873theorem powerGeneratedNativeCost_zero_calibrated {n : ℕ} (hn : n ≠ 0) :
874 PRCDoubledTraceZeroCalibrated
875 (nativeCostDoubledTrace (powerGeneratedNativeCost n)) := by
876 rw [PRCDoubledTraceZeroCalibrated, RatioOrbit.crossEq_iff_toRat_eq]
877 simp only [nativeCostDoubledTrace, doubledTraceValue, RatioOrbit.mul_toRat,
878 RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat,
879 powerGeneratedNativeCost_toRat, RatioOrbit.zero_toRat]
880 rw [zero_pow hn]
881 norm_num [jq]
882
883/-- Odd exponents reverse orientation, because an odd power remembers the sign. -/
884theorem powerGeneratedNativeCost_signReversing {n : ℕ} (hn : Odd n) :
885 PRCNativeCostSignReversing (powerGeneratedNativeCost n) := by
886 intro q r hr
887 rw [powerGeneratedNativeCost_toRat, powerGeneratedNativeCost_toRat, hr,
888 hn.neg_pow, jq_neg]
889
890/-- The cost generated by the odd power `q ↦ q^(2k+1)`. `k = 0` is the canonical
891cost; every `k ≥ 1` is a distinct point of the gauge orbit. -/
892def oddPowerGeneratedNativeCost (k : ℕ) : RatioOrbit → RatioOrbit :=
893 powerGeneratedNativeCost (2 * k + 1)
894
895theorem oddPowerGeneratedNativeCost_toRat (k : ℕ) (q : RatioOrbit) :
896 (oddPowerGeneratedNativeCost k q).toRat = jq (q.toRat ^ (2 * k + 1)) :=
897 powerGeneratedNativeCost_toRat (2 * k + 1) q
898
899theorem oddPowerGeneratedNativeCost_sansAnchor (k : ℕ) :
900 PRCStructuralNativeCostHypothesesSansAnchor (oddPowerGeneratedNativeCost k) where
901 base_sans_two := powerGeneratedNativeCost_base (2 * k + 1)
902 sign_reversing :=
903 powerGeneratedNativeCost_signReversing (n := 2 * k + 1) ⟨k, by ring⟩
904 monotone := powerGeneratedNativeCost_monotone (2 * k + 1)
905 zero_calibrated :=
906 powerGeneratedNativeCost_zero_calibrated (n := 2 * k + 1) (by omega)
907
908/-- The anchor value separates the family. The cost at the orbit `2` is
909`J(2^(2k+1))`, and `jq` is strictly increasing at or above the unit, so distinct
910exponents are distinct costs. -/
911theorem oddPowerGeneratedNativeCost_anchor_injective {k k' : ℕ} (h : k ≠ k') :
912 ¬ RatioOrbit.crossEq (oddPowerGeneratedNativeCost k two)
913 (oddPowerGeneratedNativeCost k' two) := by
914 rw [RatioOrbit.crossEq_iff_toRat_eq, oddPowerGeneratedNativeCost_toRat,
915 oddPowerGeneratedNativeCost_toRat, two_toRat]
916 have hstrict : ∀ i j : ℕ, i < j →
917 jq ((2:ℚ) ^ (2 * i + 1)) < jq ((2:ℚ) ^ (2 * j + 1)) := by
918 intro i j hij
919 refine jq_strictMono (one_le_pow₀ (by norm_num)) ?_
920 exact pow_lt_pow_right₀ (by norm_num) (by omega)
921 rcases lt_or_gt_of_ne h with hlt | hgt
922 · exact ne_of_lt (hstrict k k' hlt)
923 · exact ne_of_gt (hstrict k' k hgt)
924
925/-- The first nontrivial member: the cube cost `J(q³)`. It charges `J(8) = 49/16`
926for the orbit `2` where the canonical cost charges `J(2) = 1/4`. -/
927def cubeGeneratedNativeCost : RatioOrbit → RatioOrbit :=
928 oddPowerGeneratedNativeCost 1
929
930theorem cubeGeneratedNativeCost_toRat (q : RatioOrbit) :
931 (cubeGeneratedNativeCost q).toRat = jq (q.toRat ^ 3) :=
932 oddPowerGeneratedNativeCost_toRat 1 q
933
934theorem cubeGeneratedNativeCost_sansAnchor :
935 PRCStructuralNativeCostHypothesesSansAnchor cubeGeneratedNativeCost :=
936 oddPowerGeneratedNativeCost_sansAnchor 1
937
938/-- The canonical cost is the `k = 0` member, so the family really is a family of
939gauge choices around the answer rather than a family of impostors. -/
940theorem oddPowerGeneratedNativeCost_zero (q : RatioOrbit) :
941 (oddPowerGeneratedNativeCost 0 q).toRat = (onRatioOrbit q).toRat := by
942 rw [oddPowerGeneratedNativeCost_toRat, jq_onRatioOrbit]
943 norm_num
944
945theorem cubeGeneratedNativeCost_two_not_canonical :
946 ¬ RatioOrbit.crossEq (cubeGeneratedNativeCost two) (onRatioOrbit two) := by
947 have h := oddPowerGeneratedNativeCost_anchor_injective (k := 1) (k' := 0)
948 (by norm_num)
949 intro hcross
950 refine h ?_
951 rw [RatioOrbit.crossEq_iff_toRat_eq, oddPowerGeneratedNativeCost_zero]
952 exact crossDisp hcross
953
954/-! #### The reverse inclusion, and where the gap actually is
955
956CORRECTED TWICE ON 2026-07-25, so read the correction history as part of the
957content. The first version of this comment called the reverse inclusion a
958transcendence problem and advised against attacking it. The second version
959withdrew that, correctly, but then located the gap at the zero orbit: it said the
960open question was whether the anchor-free structural ledger implies
961`PRCDoubledTraceZeroCalibrated`. That is not a question at all.
962`PRCStructuralNativeCostHypothesesSansAnchor` carries `zero_calibrated` as its
963fourth FIELD. The ledger assumes it. Nothing is open there.
964
965The claim is that the odd power family is the WHOLE gauge orbit, stated below as
966`GaugeOrbitIsOddPowerFamily`. The two steps and their real statuses:
967
968STEP ONE, factorization, is where the whole difficulty sits, and the reason is a
969TYPE. `PRCRatioCharacter χ` has `χ : RatioOrbit → RatioOrbit`, so it demands a
970character valued in the carrier, hence rational. The d'Alembert solution of the
971composition law does not provide one. What a cost exposes is the TRACE
972`χ(q) + χ(q)⁻¹`, and carrier-valuedness of the cost is exactly rationality of the
973traces, which is strictly weaker than rationality of `χ`.
974`Cost.TraceRationalExponent.no_rational_character_at_trace_three` proves the gap
975is real and not hypothetical: the equation `r + r⁻¹ = 3` has NO rational
976solution, so a cost charging the perfectly rational `1/2` at the orbit two has no
977rational character there. The real solution is the square of the golden ratio
978(`golden_square_has_trace_three`), which the carrier provably does not contain
979(`no_native_golden_scale`).
980
981This also explains why the proved repair does not reach the anchor-free case.
982`PRCZeroCalibratedNativeCostCharacterFactorizationTarget_proved` assumes
983`PRCNativeCostHypotheses`, which INCLUDES `two_calibrated`. The extraction
984`traceRootCandidate T q = (2·T(2q) - T(q))/3` is the specialization to `χ(2) = 2`
985of `χ(q) = (T(2q) - r⁻¹T(q))/(r - r⁻¹)` with `r = χ(2)`; the anchor is what makes
986`r` known and rational. Drop the anchor and `r` is an unknown root of
987`x² - T(2)x + 1`, which need not lie in the carrier at all. So step one is: prove
988factorization through a REAL-valued character. The carrier-valued target is not
989merely unproved, it is the wrong target.
990
991STEP TWO, the exponent, is now in better shape than any previous version of this
992comment recorded, and its arithmetic core is PROVED in
993`IndisputableMonolith.Cost.TraceRationalExponent`. Given a real character, the
994round-5 cut argument makes `χ(2)` determine everything, so `χ(n) = n^c`, and an
995inhabitant outside the family is a real `c` that is not an odd integer with
996`n^c + n^(-c)` rational for every `n`. Note the weakening: TRACE rational, not
997`n^c` rational. Every previous version of this comment demanded the latter, which
998was too strong for the same reason step one was. The chain:
999
1000* trace rational makes `n^c` algebraic of degree at most two, for every `n`;
1001* six exponentials, applied to `{log 2, log 3, log 5}` and `{1, c}`, forces `c`
1002 rational, needing only that `2^c, 3^c, 5^c` be ALGEBRAIC;
1003* `int_of_rat_exponent_of_trace_rat` then forces `c` to be an integer, via
1004 `rat_of_trace_rat_of_pow_rat`: a real above one with rational trace that has
1005 any rational power is itself rational, so the quadratic case cannot survive.
1006
1007And there the chain stops: `c` is a nonnegative INTEGER and no parity cut follows.
1008Earlier versions of this comment added a fourth bullet claiming
1009`evenPowerGeneratedNativeCost_not_sansAnchor` kills the even integers. It does not.
1010That theorem says the FUNCTION `q ↦ J(q^(2k+2))` fails sign reversal, which is true
1011because an even power forgets the sign of its argument. The even EXPONENT is carried
1012by a different character, `x ↦ sgn(x)·|x|^(2k+2)`, which reverses orientation and is
1013an inhabitant (`Cost.GaugeOrbitFromRealCharacter.signedPowerNativeCost_sansAnchor`).
1014Sign reversal constrains `χ(-1)` and nothing else, so it never touched the parity.
1015
1016Only the six exponentials input is external, named as
1017`Cost.TraceRationalExponent.SixExponentialsTraceInput` rather than hidden, and
1018`exponent_is_positive_integer` is the packaged conditional.
1019
1020The Alaoglu-Erdős note stands and is worth keeping. They asked the TWO-base
1021version in 1944, whether `2^c` and `3^c` both rational forces `c` integral, and
1022that is genuinely open since it needs four exponentials. Our reduction supplies
1023every base, so it lands on the proved side.
1024
1025Net status (2026-07-26 close). The composition is DONE. Erdős's power-function step, which
1026this comment previously listed as a second external import, is now a theorem
1027(`Cost.MonotonePower.exists_exponent`, Howe's proof), and the classification is
1028`Cost.GaugeOrbitClassification.GaugeOrbitIsSignedPowerFamily_of_sixExponentials` with the
1029six exponentials input as its only hypothesis. What follows is the state of the chain as it
1030stood the day before, kept because it names the pieces.
1031
1032STEP ONE is a THEOREM:
1033`Cost.RealCharacterFactorization.SansAnchorRealCharacterFactorizationTarget_proved`.
1034Every anchor-free inhabitant factors through `realCharacterCandidate`, a real
1035character extracted by the symbolic linear root
1036`χ(q) = (r·T(2q) - T(q))/(r² - 1)` with `r = realTraceRoot(T(2))` (or the sign
1037character when `T(2) = 2`). Multiplicativity is pure d'Alembert algebra;
1038principal orientation on positive integers uses monotone cut. The algebraic
1039core (`Cost.RealTraceRoot`) and the doubled-trace RCL without the anchor remain
1040in place. What remains for the orbit claim is COMPOSITION: feed that character
1041into the MonoMult/cut gauge and apply `Cost.TraceRationalExponent` (six
1042exponentials as a named input) to force the exponent to a nonnegative integer.
1043
1044Why this matters: `Cost.UnitFromMinimality` shows the power family has a least
1045member at every exponent (`jcost_lt_pow`, `isLeastPower_iff_canonical`) and that
1046the surviving anchor is exactly the leastness condition, so closing the
1047composition would replace the last stipulation in the cost ledger with a
1048selection principle plus a nondegeneracy condition. -/
1049
1050/-- **REFUTED** as stated, and so was its first correction. Factorization through a
1051real character is
1052`Cost.RealCharacterFactorization.SansAnchorRealCharacterFactorizationTarget_proved`,
1053but the reverse inclusion into the odd-power family alone is false: the
1054zero-exponent sign member inhabits the anchor-free ledger and is not any
1055`oddPowerGeneratedNativeCost k` (`GaugeOrbitIsOddPowerFamily_refuted` in
1056`Cost/GaugeOrbitFromRealCharacter.lean`). The disjunction that replaced it,
1057`GaugeOrbitIsSignOrOddPowerFamily`, is false too, by the exponent-two member
1058`signedPowerNativeCost 1` (`GaugeOrbitIsSignOrOddPowerFamily_refuted`). What replaced
1059both is `GaugeOrbitIsSignedPowerFamily`, one inhabitant per nonnegative integer
1060exponent with character `sgn(x)·|x|^c`, and that one is PROVED, on the six
1061exponentials input alone
1062(`Cost.GaugeOrbitClassification.GaugeOrbitIsSignedPowerFamily_of_sixExponentials`).
1063Forward inclusion at every exponent is `gauge_orbit_contains_every_odd_power`
1064together with `signedPowerNativeCost_sansAnchor`. -/
1065def GaugeOrbitIsOddPowerFamily : Prop :=
1066 ∀ F : RatioOrbit → RatioOrbit, PRCStructuralNativeCostHypothesesSansAnchor F →
1067 ∃ k : ℕ, ∀ q : RatioOrbit,
1068 RatioOrbit.crossEq (F q) (oddPowerGeneratedNativeCost k q)
1069
1070/-- **The gauge orbit is infinite.** Every odd exponent gives an inhabitant of
1071the anchor-free ledger, and distinct exponents disagree at the anchor. -/
1072theorem gauge_orbit_contains_every_odd_power :
1073 ∀ k : ℕ, PRCStructuralNativeCostHypothesesSansAnchor
1074 (oddPowerGeneratedNativeCost k) ∧
1075 ∀ k' : ℕ, k ≠ k' → ¬ RatioOrbit.crossEq (oddPowerGeneratedNativeCost k two)
1076 (oddPowerGeneratedNativeCost k' two) :=
1077 fun k => ⟨oddPowerGeneratedNativeCost_sansAnchor k,
1078 fun _ h => oddPowerGeneratedNativeCost_anchor_injective h⟩
1079
1080/-- **The anchor is a genuine unit gauge.** The anchor-free structural ledger
1081does NOT force the canonical cost. Everything else in the ledger is structure;
1082the last field is a choice of unit. -/
1083theorem PRCStructuralSansAnchorUniquenessTarget_refuted :
1084 ¬ PRCStructuralSansAnchorUniquenessTarget := by
1085 intro huniq
1086 exact cubeGeneratedNativeCost_two_not_canonical
1087 (huniq cubeGeneratedNativeCost cubeGeneratedNativeCost_sansAnchor two)
1088
1089/-! ### The carrier is strictly more rigid than the line
1090
1091`composition_law_admits_full_scale_family` says that on the completed line the
1092composition law admits `costLambda l x = J(x^l)` for EVERY real `l > 0`: the
1093continuum gauge orbit is uncountable, and `calibrationAxiom` has to collapse all
1094of it. The free side does not inherit that whole family. What is proved below is
1095one exclusion, and it is proved without calibration:
1096
1097* The function `q ↦ J(q^(2k+2))` is a perfectly good carrier function. It
1098 satisfies every field of the anchor-free structural ledger EXCEPT sign
1099 reversal, and sign reversal kills it, with no anchor and no calibration
1100 anywhere. Read this as a statement about that function and NOT about even
1101 exponents: the character `sgn(x)·|x|^(2k+2)` has the same absolute value, does
1102 reverse orientation, and is an inhabitant
1103 (`Cost.GaugeOrbitFromRealCharacter.signedPowerNativeCost_sansAnchor`).
1104 Conflating the two cost this program a false classification for two years.
1105
1106`l = 2` is the sharp case, because it is the continuum's own headline
1107countermodel: `composition_law_without_calibration_does_not_force_jcost`
1108exhibits `costLambdaTwo` as a function satisfying every continuum hypothesis
1109except calibration. On the carrier that same cost is not merely uncalibrated, it
1110is REFUTED, by an axiom that says a debit read backwards is a credit.
1111
1112WHAT IS NOT PROVED HERE, stated so that nobody reads the above as more than it
1113is. The non-integer exponents are NOT excluded in this module. It is tempting to
1114say they cannot define a carrier function because the carrier is rational, and
1115that is wrong twice over: `2 ^ (logb 2 3) = 3` is rational at a non-integer
1116exponent, and in any case the carrier only constrains the TRACE `n^c + n^(-c)`,
1117not `n^c` itself. The correct question is whether the trace can stay rational at
1118every `n` without `c` being an integer. Corrected 2026-07-25: that is no longer
1119the wall. `Cost.TraceRationalExponent.int_of_rat_exponent_of_trace_rat` settles
1120the rational-exponent case outright, and six exponentials settles the irrational
1121one, so the exponent is an integer. The surviving wall is the factorization step
1122recorded above at `GaugeOrbitIsOddPowerFamily`, and the comparison below is the
1123even-exponent exclusion plus the odd-power witnesses, nothing wider.
1124
1125Within that scope the answer to "is the calibration axiom the price of the
1126continuum or the price of calibration as such" is: at least partly the former.
1127The line admits a family the carrier provably does not, and the axiom is paying
1128for the difference. -/
1129
1130/-- The cost generated by the even power `q ↦ q^(2k+2)`. -/
1131def evenPowerGeneratedNativeCost (k : ℕ) : RatioOrbit → RatioOrbit :=
1132 powerGeneratedNativeCost (2 * k + 2)
1133
1134/-- The carrier analogue of the continuum countermodel `costLambdaTwo`. -/
1135def squareGeneratedNativeCost : RatioOrbit → RatioOrbit :=
1136 evenPowerGeneratedNativeCost 0
1137
1138/-- **Even powers fail sign reversal, and nothing else.** An even power cannot
1139tell `-q` from `q`, so orientation reversal would force the cost to be constantly
1140`-1`, which it is not at the anchor. -/
1141theorem powerGeneratedNativeCost_not_signReversing {n : ℕ} (hn : Even n) :
1142 ¬ PRCNativeCostSignReversing (powerGeneratedNativeCost n) := by
1143 intro h
1144 have hr : (ratioOrbitOfRat (-2 : ℚ)).toRat = -two.toRat := by
1145 rw [ratioOrbitOfRat_toRat, two_toRat]
1146 have hsign := h two (ratioOrbitOfRat (-2 : ℚ)) hr
1147 have hneg : ((-2 : ℚ)) ^ n = (2 : ℚ) ^ n := hn.neg_pow 2
1148 rw [powerGeneratedNativeCost_toRat, powerGeneratedNativeCost_toRat,
1149 ratioOrbitOfRat_toRat, two_toRat, hneg] at hsign
1150 have hpos : (0 : ℚ) < 2 ^ n := by positivity
1151 have hnn := jq_nonneg hpos
1152 linarith
1153
1154/-- Everything except orientation. The even-power costs satisfy the whole
1155anchor-free ledger apart from sign reversal, so the exclusion is attributable to
1156exactly one field. -/
1157theorem evenPowerGeneratedNativeCost_sans_signReversing (k : ℕ) :
1158 PRCNativeCostHypothesesSansTwoCalibration (evenPowerGeneratedNativeCost k) ∧
1159 PRCNativeCostMonotone (evenPowerGeneratedNativeCost k) ∧
1160 PRCDoubledTraceZeroCalibrated
1161 (nativeCostDoubledTrace (evenPowerGeneratedNativeCost k)) :=
1162 ⟨powerGeneratedNativeCost_base (2 * k + 2),
1163 powerGeneratedNativeCost_monotone (2 * k + 2),
1164 powerGeneratedNativeCost_zero_calibrated (n := 2 * k + 2) (by omega)⟩
1165
1166theorem evenPowerGeneratedNativeCost_not_sansAnchor (k : ℕ) :
1167 ¬ PRCStructuralNativeCostHypothesesSansAnchor
1168 (evenPowerGeneratedNativeCost k) := by
1169 intro h
1170 exact powerGeneratedNativeCost_not_signReversing
1171 (n := 2 * k + 2) ⟨k + 1, by ring⟩ h.sign_reversing
1172
1173/-- **The free side refutes the continuum's countermodel without calibrating.**
1174The `λ = 2` cost is the exact function the continuum theorem cannot exclude
1175without the calibration hypothesis. Its carrier analogue satisfies every other
1176structural field and is excluded by orientation reversal alone. -/
1177theorem native_ledger_refutes_the_square_cost :
1178 (PRCNativeCostHypothesesSansTwoCalibration squareGeneratedNativeCost ∧
1179 PRCNativeCostMonotone squareGeneratedNativeCost ∧
1180 PRCDoubledTraceZeroCalibrated
1181 (nativeCostDoubledTrace squareGeneratedNativeCost)) ∧
1182 ¬ PRCStructuralNativeCostHypothesesSansAnchor squareGeneratedNativeCost :=
1183 ⟨evenPowerGeneratedNativeCost_sans_signReversing 0,
1184 evenPowerGeneratedNativeCost_not_sansAnchor 0⟩
1185
1186/-- **The continuum scale family does not transport.** On the line every
1187positive real exponent is an admissible cost. On the carrier the even exponents
1188are refuted outright, so part of what `calibrationAxiom` collapses is freedom
1189that exists only after completion.
1190
1191This does NOT say the carrier orbit is smaller as a cardinality. It says one
1192identified subfamily of the continuum orbit is absent from the carrier orbit.
1193The odd exponents are present (`gauge_orbit_contains_every_odd_power`), and
1194whether anything else is present is the named transcendence wall above. -/
1195theorem continuum_gauge_exceeds_native_gauge :
1196 (∀ l : ℝ, 0 < l →
1197 Cost.FunctionalEquation.IsReciprocalCost (costLambda l) ∧
1198 Cost.FunctionalEquation.IsNormalized (costLambda l) ∧
1199 Cost.FunctionalEquation.SatisfiesCompositionLaw (costLambda l) ∧
1200 ContinuousOn (costLambda l) (Set.Ioi 0)) ∧
1201 (∀ k : ℕ, ¬ PRCStructuralNativeCostHypothesesSansAnchor
1202 (evenPowerGeneratedNativeCost k)) :=
1203 ⟨fun l hl => composition_law_admits_full_scale_family l hl,
1204 evenPowerGeneratedNativeCost_not_sansAnchor⟩
1205
1206/-- The continuum gauge orbit, as a set of functions on the line. -/
1207def continuumScaleFamily : Set (ℝ → ℝ) :=
1208 {F | ∃ l : ℝ, 0 < l ∧ F = costLambda l}
1209
1210/-- **The continuum gauge orbit is uncountable.** Distinct positive exponents
1211give distinct costs (`costLambda_injective`) and the positive reals are
1212uncountable, so what `calibrationAxiom` collapses on the line is not a discrete
1213list of impostors. Stated here rather than left as a remark, because the size of
1214the collapsed family is the quantitative half of the comparison with the
1215carrier. -/
1216theorem continuum_scale_family_uncountable :
1217 ¬ continuumScaleFamily.Countable := by
1218 intro hc
1219 haveI : Countable continuumScaleFamily := hc.to_subtype
1220 have hinj : Function.Injective
1221 (fun l : Set.Ioi (0 : ℝ) =>
1222 (⟨costLambda (l : ℝ), ⟨(l : ℝ), Set.mem_Ioi.mp l.2, rfl⟩⟩ :
1223 continuumScaleFamily)) := by
1224 rintro ⟨l, hl⟩ ⟨m, hm⟩ h
1225 have hfun : costLambda l = costLambda m := congrArg Subtype.val h
1226 exact Subtype.ext (costLambda_injective (Set.mem_Ioi.mp hl) (Set.mem_Ioi.mp hm)
1227 (fun x => congrFun hfun x))
1228 haveI : Countable (Set.Ioi (0 : ℝ)) := hinj.countable
1229 have hexp : Function.Injective
1230 (fun x : ℝ => (⟨Real.exp x, Set.mem_Ioi.mpr (Real.exp_pos x)⟩ :
1231 Set.Ioi (0 : ℝ))) := by
1232 intro a b h
1233 exact Real.exp_injective (congrArg Subtype.val h)
1234 exact real_not_countable hexp.countable
1235
1236/-- **The line's monotone class is exactly the scale family.** One name for both
1237inclusions: every positive exponent is admissible and continuous, and
1238conversely any reciprocal, normalized, composition-obeying cost that is monotone
1239is `costLambda c` for a single real `c`. The converse needs no continuity and no
1240completeness, so the honest continuum comparison is monotone against monotone,
1241not monotone against continuous. -/
1242theorem continuum_monotone_class_is_the_scale_family :
1243 (∀ l : ℝ, 0 < l →
1244 Cost.FunctionalEquation.IsReciprocalCost (costLambda l) ∧
1245 Cost.FunctionalEquation.IsNormalized (costLambda l) ∧
1246 Cost.FunctionalEquation.SatisfiesCompositionLaw (costLambda l) ∧
1247 ContinuousOn (costLambda l) (Set.Ioi 0)) ∧
1248 (∀ F : ℝ → ℝ,
1249 Cost.FunctionalEquation.IsReciprocalCost F →
1250 Cost.FunctionalEquation.IsNormalized F →
1251 Cost.FunctionalEquation.SatisfiesCompositionLaw F →
1252 MonotoneOn (Cost.FunctionalEquation.H F) (Set.Ici (0 : ℝ)) →
1253 ∃ c : ℝ, ∀ x : ℝ, 0 < x → F x = costLambda c x) :=
1254 ⟨fun l hl => composition_law_admits_full_scale_family l hl,
1255 fun F hR hN hC hM => composition_law_monotone_forces_costLambda F hR hN hC hM⟩
1256
1257/-- The square cost also misses the anchor, since `J(4) ≠ J(2)`. Sign reversal
1258already refutes it, so this is the redundant second failure, recorded because
1259the paper states it. -/
1260theorem squareGeneratedNativeCost_two_not_canonical :
1261 ¬ RatioOrbit.crossEq (squareGeneratedNativeCost two) (onRatioOrbit two) := by
1262 rw [RatioOrbit.crossEq_iff_toRat_eq, jq_onRatioOrbit,
1263 squareGeneratedNativeCost, evenPowerGeneratedNativeCost,
1264 powerGeneratedNativeCost_toRat, two_toRat]
1265 norm_num [jq]
1266
1267/-! ### Gauge rigidity: the anchor is the only choice -/
1268
1269theorem character_display {χ : RatioOrbit → RatioOrbit}
1270 (hχ : PRCRatioCharacter χ) {a b : RatioOrbit} (hab : a.toRat = b.toRat) :
1271 (χ a).toRat = (χ b).toRat :=
1272 crossDisp
1273 (PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical hχ
1274 PRCNormalizeRatioCanonicalTarget_proved a b (dispCross hab))
1275
1276/-- The arithmetic data a monotone factorized cost leaves on the positive
1277integers. -/
1278theorem monoMult_of_character {F χ : RatioOrbit → RatioOrbit}
1279 (hmono : PRCNativeCostMonotone F)
1280 (hχ : PRCRatioCharacter χ)
1281 (hFχ : ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (costFromCharacter χ q)) :
1282 MonoMult (fun n : ℕ => (χ (natOrbit n)).toRat) := by
1283 have hFdisp : ∀ q : RatioOrbit, (F q).toRat = jq ((χ q).toRat) := by
1284 intro q
1285 rw [crossDisp (hFχ q), costFromCharacter_jq]
1286 refine
1287 { ne := ?_, one := ?_, mul := ?_, mono := ?_ }
1288 · intro n hn
1289 refine hχ.nonzero_preserving ?_
1290 rw [natOrbit_toRat]
1291 exact_mod_cast Nat.one_le_iff_ne_zero.mp hn
1292 · show (χ (natOrbit 1)).toRat = 1
1293 have h1 : (natOrbit 1).toRat = RatioOrbit.one.toRat := by
1294 rw [natOrbit_toRat, RatioOrbit.one_toRat]; norm_num
1295 rw [character_display hχ h1, crossDisp hχ.unit, RatioOrbit.one_toRat]
1296 · intro m n _ _
1297 show (χ (natOrbit (m * n))).toRat
1298 = (χ (natOrbit m)).toRat * (χ (natOrbit n)).toRat
1299 have hdisp : (natOrbit (m * n)).toRat =
1300 (RatioOrbit.mul (natOrbit m) (natOrbit n)).toRat := by
1301 rw [natOrbit_toRat, RatioOrbit.mul_toRat, natOrbit_toRat, natOrbit_toRat]
1302 push_cast
1303 ring
1304 rw [character_display hχ hdisp,
1305 crossDisp (hχ.multiplicative (natOrbit m) (natOrbit n)),
1306 RatioOrbit.mul_toRat]
1307 · intro m n hm hmn
1308 have hstep := hmono (natOrbit m) (natOrbit n) (natOrbit_isPosInt hm)
1309 (natOrbit_isPosInt (le_trans hm hmn)) (by
1310 rw [natOrbit_toRat, natOrbit_toRat]; exact_mod_cast hmn)
1311 rw [hFdisp, hFdisp] at hstep
1312 exact hstep
1313
1314/-- The reciprocal of a monotone character is a monotone character with the
1315same cost. -/
1316theorem MonoMult.inv {h : ℕ → ℚ} (H : MonoMult h) :
1317 MonoMult (fun k => (h k)⁻¹) where
1318 ne := fun k hk => inv_ne_zero (H.ne k hk)
1319 one := by show (h 1)⁻¹ = 1; rw [H.one]; norm_num
1320 mul := fun a b ha hb => by
1321 show (h (a * b))⁻¹ = (h a)⁻¹ * (h b)⁻¹
1322 rw [H.mul a b ha hb, mul_inv]
1323 mono := fun a b ha hab => by
1324 show jq ((h a)⁻¹) ≤ jq ((h b)⁻¹)
1325 rw [jq_inv, jq_inv]
1326 exact H.mono a b ha hab
1327
1328/-- The anchor of a monotone character is positive. A negative anchor would make
1329the fourth orbit cost more than the eighth. -/
1330theorem MonoMult.two_pos {h : ℕ → ℚ} (H : MonoMult h) : 0 < h 2 := by
1331 rcases lt_trichotomy (h 2) 0 with hlt | heq | hgt
1332 · exfalso
1333 have h4 : h 4 = (h 2) ^ 2 := by
1334 have he : (4:ℕ) = 2 ^ 2 := by norm_num
1335 rw [he, H.pow 2 2 (by norm_num)]
1336 have h8 : h 8 = (h 2) ^ 3 := by
1337 have he : (8:ℕ) = 2 ^ 3 := by norm_num
1338 rw [he, H.pow 2 3 (by norm_num)]
1339 have hmm := H.mono 4 8 (by norm_num) (by norm_num)
1340 rw [h4, h8] at hmm
1341 have hp4 : (0:ℚ) < (h 2) ^ 2 := pow_two_pos_of_ne_zero (H.ne 2 (by norm_num))
1342 have hn8 : (h 2) ^ 3 < 0 := by nlinarith
1343 have hj4 := jq_nonneg hp4
1344 have hj8 := jq_lt_zero hn8
1345 linarith
1346 · exact absurd heq (H.ne 2 (by norm_num))
1347 · exact hgt
1348
1349/-- Orientation: replacing a monotone character by its reciprocal changes no
1350cost, and one of the two carries its anchor at or above the unit. -/
1351theorem MonoMult.orient {h : ℕ → ℚ} (H : MonoMult h) :
1352 ∃ h' : ℕ → ℚ, MonoMult h' ∧ 1 ≤ h' 2 ∧ ∀ n : ℕ, jq (h' n) = jq (h n) := by
1353 rcases le_or_gt 1 (h 2) with hle | hlt
1354 · exact ⟨h, H, hle, fun _ => rfl⟩
1355 · refine ⟨fun k => (h k)⁻¹, H.inv, ?_, fun n => jq_inv (h n)⟩
1356 show (1:ℚ) ≤ (h 2)⁻¹
1357 have h2pos := H.two_pos
1358 have hcancel : h 2 * (h 2)⁻¹ = 1 := mul_inv_cancel₀ (ne_of_gt h2pos)
1359 nlinarith [inv_pos.mpr h2pos]
1360
1361theorem jq_inj_ge_one {s t : ℚ} (hs : 1 ≤ s) (ht : 1 ≤ t) (hj : jq s = jq t) :
1362 s = t :=
1363 le_antisymm (jq_le_reflect hs ht (le_of_eq hj))
1364 (jq_le_reflect ht hs (le_of_eq hj.symm))
1365
1366/-- **Gauge rigidity.** Two monotone costs that factor through characters and
1367agree at the single orbit `2` agree on every positive integer orbit. Combined
1368with the cube witness: the anchor is a real choice, and it is the only one. That
1369is the free-side stratification, form forced and unit free. -/
1370theorem structural_gauge_rigidity
1371 {F₁ F₂ χ₁ χ₂ : RatioOrbit → RatioOrbit}
1372 (hm₁ : PRCNativeCostMonotone F₁) (hm₂ : PRCNativeCostMonotone F₂)
1373 (hχ₁ : PRCRatioCharacter χ₁) (hχ₂ : PRCRatioCharacter χ₂)
1374 (hf₁ : ∀ q : RatioOrbit, RatioOrbit.crossEq (F₁ q) (costFromCharacter χ₁ q))
1375 (hf₂ : ∀ q : RatioOrbit, RatioOrbit.crossEq (F₂ q) (costFromCharacter χ₂ q))
1376 (hanchor : RatioOrbit.crossEq (F₁ two) (F₂ two)) :
1377 ∀ a : RatioOrbit, IsPosIntOrbit a → RatioOrbit.crossEq (F₁ a) (F₂ a) := by
1378 have hd₁ : ∀ q : RatioOrbit, (F₁ q).toRat = jq ((χ₁ q).toRat) := fun q => by
1379 rw [crossDisp (hf₁ q), costFromCharacter_jq]
1380 have hd₂ : ∀ q : RatioOrbit, (F₂ q).toRat = jq ((χ₂ q).toRat) := fun q => by
1381 rw [crossDisp (hf₂ q), costFromCharacter_jq]
1382 obtain ⟨k₁, Hk₁, hk₁, hj₁⟩ := (monoMult_of_character hm₁ hχ₁ hf₁).orient
1383 obtain ⟨k₂, Hk₂, hk₂, hj₂⟩ := (monoMult_of_character hm₂ hχ₂ hf₂).orient
1384 have htwodisp : (natOrbit 2).toRat = two.toRat := by
1385 rw [natOrbit_toRat, two_toRat]; norm_num
1386 have hanch : jq (k₁ 2) = jq (k₂ 2) := by
1387 rw [hj₁ 2, hj₂ 2]
1388 show jq ((χ₁ (natOrbit 2)).toRat) = jq ((χ₂ (natOrbit 2)).toRat)
1389 rw [character_display hχ₁ htwodisp, character_display hχ₂ htwodisp,
1390 ← hd₁ two, ← hd₂ two, crossDisp hanchor]
1391 have hkeq := monoMult_gauge Hk₁ Hk₂ (jq_inj_ge_one hk₁ hk₂ hanch) hk₁
1392 rintro a ⟨n, hn, han⟩
1393 have hdisp : a.toRat = (natOrbit n).toRat := by rw [natOrbit_toRat, han]
1394 refine dispCross ?_
1395 rw [hd₁, hd₂, character_display hχ₁ hdisp, character_display hχ₂ hdisp]
1396 show jq ((fun m : ℕ => (χ₁ (natOrbit m)).toRat) n)
1397 = jq ((fun m : ℕ => (χ₂ (natOrbit m)).toRat) n)
1398 rw [← hj₁ n, ← hj₂ n, hkeq n hn]
1399
1400/-! ### The round-6 certificate -/
1401
1402/-- **The free-side stratification.** On the countable carrier the form of the
1403cost is forced by arithmetic alone and the only residual freedom is the size of
1404the unit, fixed by one anchor. -/
1405structure StructuralStratificationCertificate : Prop where
1406 /-- The structural ledger forces the canonical cost. -/
1407 uniqueness : PRCStructuralNativeCostUniquenessTarget
1408 /-- Two of its four fields never mention the canonical cost, and the ledger it
1409 replaces is recovered in full. -/
1410 contracts_slim :
1411 ∀ F : RatioOrbit → RatioOrbit, PRCStructuralNativeCostHypotheses F →
1412 PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses F
1413 /-- Positivity is derived, not assumed. -/
1414 positivity :
1415 ∀ F : RatioOrbit → RatioOrbit, PRCStructuralNativeCostHypotheses F →
1416 PRCNativeCostPositive F
1417 /-- The remaining anchor is a genuine unit gauge: without it the ledger admits
1418 the cube cost. -/
1419 gauge_inhabited : ¬ PRCStructuralSansAnchorUniquenessTarget
1420 /-- And the gauge orbit is infinite: one inhabitant per odd exponent, pairwise
1421 distinguished by their value at the anchor. -/
1422 gauge_orbit_infinite :
1423 ∀ k : ℕ, PRCStructuralNativeCostHypothesesSansAnchor
1424 (oddPowerGeneratedNativeCost k) ∧
1425 ∀ k' : ℕ, k ≠ k' → ¬ RatioOrbit.crossEq (oddPowerGeneratedNativeCost k two)
1426 (oddPowerGeneratedNativeCost k' two)
1427 /-- And it is the only gauge: the anchor value determines every positive
1428 integer orbit. -/
1429 gauge_rigid :
1430 ∀ F₁ F₂ χ₁ χ₂ : RatioOrbit → RatioOrbit,
1431 PRCNativeCostMonotone F₁ → PRCNativeCostMonotone F₂ →
1432 PRCRatioCharacter χ₁ → PRCRatioCharacter χ₂ →
1433 (∀ q, RatioOrbit.crossEq (F₁ q) (costFromCharacter χ₁ q)) →
1434 (∀ q, RatioOrbit.crossEq (F₂ q) (costFromCharacter χ₂ q)) →
1435 RatioOrbit.crossEq (F₁ two) (F₂ two) →
1436 ∀ a : RatioOrbit, IsPosIntOrbit a →
1437 RatioOrbit.crossEq (F₁ a) (F₂ a)
1438 /-- The class is inhabited. -/
1439 nonvacuous : PRCStructuralNativeCostHypotheses canonicalSelectedNativeCost
1440
1441/-! ## Part 8 (ROUND 8): where the completion is actually bought
1442
1443The public spine tags the reciprocal-generator claim at `traceClosure` because
1444the certificate lives on ℝ. Three of its four facts do not need to. The
1445involution, the reciprocal symmetry of the cost, and the characterization of the
1446unit as the unique zero-cost orbit are all δ-native, and are proved here on the
1447carrier. The fourth is where the completion is genuinely bought, and this
1448section proves exactly that: the self-similar scale `1 + 1/x = x` has NO
1449solution in the δ-native carrier. Same shape as the cost result. The form is
1450forced; the completion is a purchase, and now the purchase has a receipt. -/
1451
1452theorem native_recip_involutive (q : RatioOrbit) :
1453 (RatioOrbit.recip (RatioOrbit.recip q)).toRat = q.toRat := by
1454 rw [RatioOrbit.recip_toRat, RatioOrbit.recip_toRat, inv_inv]
1455
1456theorem native_cost_recip_symmetric (q : RatioOrbit) :
1457 (onRatioOrbit (RatioOrbit.recip q)).toRat = (onRatioOrbit q).toRat := by
1458 rw [jq_onRatioOrbit, jq_onRatioOrbit, RatioOrbit.recip_toRat, jq_inv]
1459
1460/-- On the positive cone the reciprocal fixes exactly the zero-cost orbit: the
1461unit is the only thing that costs nothing, and it is the only self-reciprocal
1462positive orbit. -/
1463theorem native_recip_fixed_iff_cost_zero {q : RatioOrbit} (hq : 0 < q.toRat) :
1464 (RatioOrbit.recip q).toRat = q.toRat ↔ (onRatioOrbit q).toRat = 0 := by
1465 rw [RatioOrbit.recip_toRat, jq_onRatioOrbit]
1466 constructor
1467 · intro h
1468 have hne : q.toRat ≠ 0 := ne_of_gt hq
1469 have hsq : q.toRat * q.toRat = 1 := by
1470 field_simp at h
1471 linarith [h]
1472 have ht : q.toRat = 1 := by nlinarith [hq, hsq]
1473 rw [ht, jq_one]
1474 · intro h
1475 rw [jq_eq_zero (ne_of_gt hq) h]
1476 norm_num
1477
1478/-- **The golden scale has no δ-native solution.** Elementary and choice-free:
1479clearing denominators gives `a² = b(a+b)` in lowest terms, so the denominator
1480divides `a²` and is therefore `1`, and no integer solves `a² = a + 1`. -/
1481theorem no_rat_golden_scale {t : ℚ} (ht : 0 < t) : 1 + t⁻¹ ≠ t := by
1482 intro h
1483 have ht0 : t ≠ 0 := ne_of_gt ht
1484 have hsq : t * t = t + 1 := by
1485 field_simp at h
1486 linarith [h]
1487 have hdpos : (0:ℚ) < (t.den : ℚ) := by exact_mod_cast t.pos
1488 have hnd : (t.num : ℚ) = t * (t.den : ℚ) :=
1489 (div_eq_iff (ne_of_gt hdpos)).mp (Rat.num_div_den t)
1490 have hkey : (t.num : ℚ) * (t.num : ℚ)
1491 = (t.num : ℚ) * (t.den : ℚ) + (t.den : ℚ) * (t.den : ℚ) := by
1492 rw [hnd]
1493 linear_combination ((t.den : ℚ) * (t.den : ℚ)) * hsq
1494 have hZ : t.num * t.num = t.num * (t.den : ℤ) + (t.den : ℤ) * (t.den : ℤ) := by
1495 exact_mod_cast hkey
1496 have hdvd : (t.den : ℤ) ∣ t.num * t.num := ⟨t.num + (t.den : ℤ), by
1497 rw [hZ]; ring⟩
1498 have hdvdN : t.den ∣ t.num.natAbs * t.num.natAbs := by
1499 have hstep := Int.natAbs_dvd_natAbs.mpr hdvd
1500 simpa [Int.natAbs_mul] using hstep
1501 have hcop : Nat.Coprime t.den (t.num.natAbs * t.num.natAbs) :=
1502 Nat.Coprime.mul_right t.reduced.symm t.reduced.symm
1503 have hd1 : t.den = 1 := by
1504 have hg : Nat.gcd t.den (t.num.natAbs * t.num.natAbs) = t.den :=
1505 Nat.gcd_eq_left hdvdN
1506 rw [Nat.Coprime] at hcop
1507 rw [hcop] at hg
1508 exact hg.symm
1509 rw [hd1] at hZ
1510 push_cast at hZ
1511 have hpos : 0 < t.num := Rat.num_pos.mpr ht
1512 have hb : t.num ≤ 2 := by nlinarith [hZ, sq_nonneg (t.num - 1)]
1513 have hcase : t.num = 1 ∨ t.num = 2 := by omega
1514 rcases hcase with hc | hc <;> rw [hc] at hZ <;> norm_num at hZ
1515
1516/-- The carrier statement: no orbit is the self-similar scale. -/
1517theorem no_native_golden_scale :
1518 ¬ ∃ q : RatioOrbit, 0 < q.toRat ∧ 1 + (q.toRat)⁻¹ = q.toRat := by
1519 rintro ⟨q, hq, h⟩
1520 exact no_rat_golden_scale hq h
1521
1522/-- **The φ split.** Everything the reciprocal generator says about the cost is
1523δ-native; only the fixed point is bought. -/
1524structure NativeReciprocalGeneratorSplit : Prop where
1525 involutive : ∀ q : RatioOrbit,
1526 (RatioOrbit.recip (RatioOrbit.recip q)).toRat = q.toRat
1527 cost_symmetric : ∀ q : RatioOrbit,
1528 (onRatioOrbit (RatioOrbit.recip q)).toRat = (onRatioOrbit q).toRat
1529 unit_is_cost_zero : ∀ q : RatioOrbit, 0 < q.toRat →
1530 ((RatioOrbit.recip q).toRat = q.toRat ↔ (onRatioOrbit q).toRat = 0)
1531 scale_is_a_purchase :
1532 ¬ ∃ q : RatioOrbit, 0 < q.toRat ∧ 1 + (q.toRat)⁻¹ = q.toRat
1533
1534theorem nativeReciprocalGeneratorSplit_holds : NativeReciprocalGeneratorSplit where
1535 involutive := native_recip_involutive
1536 cost_symmetric := native_cost_recip_symmetric
1537 unit_is_cost_zero := fun _ hq => native_recip_fixed_iff_cost_zero hq
1538 scale_is_a_purchase := no_native_golden_scale
1539
1540theorem structuralStratificationCertificate_holds :
1541 StructuralStratificationCertificate where
1542 uniqueness := PRCStructuralNativeCostUniquenessTarget_proved
1543 contracts_slim := structural_forces_slim
1544 positivity := structural_forces_positive
1545 gauge_inhabited := PRCStructuralSansAnchorUniquenessTarget_refuted
1546 gauge_orbit_infinite := gauge_orbit_contains_every_odd_power
1547 gauge_rigid := fun _ _ _ _ hm₁ hm₂ hχ₁ hχ₂ hf₁ hf₂ ha =>
1548 structural_gauge_rigidity hm₁ hm₂ hχ₁ hχ₂ hf₁ hf₂ ha
1549 nonvacuous := canonicalSelectedNativeCost_structural_hypotheses
1550
1551/-! ### Axiom audit
1552
1553The load-bearing results of this module, printed so the build log carries the
1554receipt. Anything beyond `propext`, `Classical.choice`, and `Quot.sound` (in
1555particular `sorryAx`) means a claim resting on this file is not proved. -/
1556
1557#print axioms PRCStructuralNativeCostUniquenessTarget_proved
1558#print axioms PRCSignReversingNativeCostUniquenessTarget_proved
1559#print axioms PRCStructuralSansAnchorUniquenessTarget_refuted
1560#print axioms gauge_orbit_contains_every_odd_power
1561#print axioms oddPowerGeneratedNativeCost_sansAnchor
1562#print axioms powerGeneratedNativeCost_signReversing
1563#print axioms powerGeneratedNativeCost_not_signReversing
1564#print axioms native_ledger_refutes_the_square_cost
1565#print axioms continuum_gauge_exceeds_native_gauge
1566#print axioms continuum_scale_family_uncountable
1567#print axioms continuum_monotone_class_is_the_scale_family
1568#print axioms squareGeneratedNativeCost_two_not_canonical
1569#print axioms no_native_golden_scale
1570#print axioms nativeReciprocalGeneratorSplit_holds
1571#print axioms structuralStratificationCertificate_holds
1572
1573end PRCJCost
1574end PrimitiveRecognitionCalculus
1575end Foundation
1576end IndisputableMonolith
1577