IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimalityCertificate
IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostMinimalityCertificate.lean · 832 lines · 60 declarations
show as:
view math explainer →
1/-
2 PrimitiveRecognitionCalculus/PRCNativeCostMinimalityCertificate.lean
3
4 Round-trip source:
5 δ/plans/JCost_SlimLedger_Minimality_Certificate_Prereg_20260724.json (frozen)
6 plans/Delta_JCost_Slim_Ledger_Minimality_Certificate_Session_Prompt_20260724.txt
7
8 Field-by-field minimality certificate for the slim native-cost ledger
9 (P-delta-jfree, round 3). Round 2 (`PRCNativeCostMinimality.lean`) proved
10 that the slim ledger (base: reciprocity, normalization invariance, nonzero
11 RCL, unit-zero, two-calibration; plus prime-pair products, signed unit, and
12 zero orbit) forces the canonical J-cost on `RatioOrbit`, and that the
13 all-prime axis family is redundant. This module settles what remained: every
14 removable calibration field of the slim ledger is NECESSARY. For each such
15 field we define the class "slim minus this field" (connected to the slim
16 ledger by a bridging iff) and refute its uniqueness target with an explicit
17 countermodel:
18
19 * TWO-POINT ANCHOR (`two_calibrated`), the new construction of this round:
20 the Liouville sign twist. `liouvilleSign t = (-1)^(Ω num + Ω den)` is the
21 parity of the total prime-exponent sum of the reduced fraction (Mathlib
22 totalizes `Ω 0 = 0`, so the sign is `+1` at `0`, where it is harmless);
23 the twisted cost displays `J(liouvilleSign t · t)`. The sign is completely
24 multiplicative on nonzero rationals (the reduced-fraction cross identity
25 keeps the parity), equal to `-1` on every prime, hence `+1` on every
26 product of two primes and at the signed unit. The twisted cost therefore
27 passes reciprocity, normalization invariance, the nonzero RCL, unit-zero,
28 prime-pair products, the signed unit, and the zero orbit, and fails
29 exactly the two-point anchor: it displays `J(-2) = -9/4` at orbit 2
30 against the canonical `J(2) = 1/4`.
31
32 * PAIR FIELD (`prime_pair_product_cost`): the parent module's two-adic
33 axis-twist cost. It satisfies the full base (including two-calibration:
34 J-reciprocity hides the inversion on its own axis); this module adds the
35 signed-unit and zero-orbit fields (the twist fixes `-1` and `0` since
36 both have zero 2-adic valuation displays), and the parent already proves
37 it fails prime-pair products at the mixed (2,3) orbit.
38
39 * SIGNED UNIT (`signed_unit`): the parent module's absolute-value cost.
40 The parent already proves base + pairs + zero-orbit calibration and the
41 failure at `-1`; this round only repackages against the sans-sign class.
42
43 * ZERO ORBIT (`zero_calibrated`): round 2's refutation of
44 `PRCSignedStrengthenedNativeCostUniquenessTarget` by the zero-flat
45 witness, reused verbatim.
46
47 The terminal deposit `SlimLedgerMinimalityCertificate` bundles the round-2
48 uniqueness theorem with the four necessity refutations. Tag deliberation:
49 the prompt allowed `classicalExtension` (round 1's wall convention), but
50 all cost domains and codomains here are `RatioOrbit` and all display
51 arithmetic is discrete; the stock witnesses are arithmetically explicit,
52 although some parent wrappers use eliminable classical equality tests, and
53 the targets quantify over the function type `RatioOrbit → RatioOrbit`
54 exactly as the round-1/2 deposits already tagged `deltaOnly` do. No
55 completed carrier, continuum object, or continuity premise appears in any
56 statement or witness; round 1's wall was `classicalExtension` because its
57 subject was the continuum price, which is absent here. The certificate is
58 therefore minted at `deltaOnly`; the axiom audit (standard basis) is
59 printed at the bottom. (Cross-family review: Codex gpt-5.6-sol xhigh,
60 2026-07-24, verdict MINT; tag reasoning endorsed with this wording.)
61
62 Preregistered bonus (Part 5b): the nonzero RCL core is ALSO necessary,
63 witnessed by the `5`-spike (canonical J displays everywhere except the
64 `5`- and `1/5`-displays, sent to `0`): no retained calibration probe
65 reaches orbit `5`, so the spike inhabits "slim minus RCL" and differs from
66 J there. The frozen certificate keeps its preregistered five-field shape;
67 the bonus is a separate deposit (`PRCSlimSansRclUniquenessTarget_refuted`).
68
69 Scope note: the remaining base structural fields (reciprocity,
70 normalization invariance, unit-zero) define what a native cost IS rather
71 than calibrating it against J; their individual necessity is out of scope
72 here and stays OPEN (recorded in the prereg).
73
74 Scope: reads `PRCNativeCostMinimality.lean` (and through it the round-1
75 module and the parent). It edits none of them and never touches
76 `cost_selection_holds`, `cost_selection_native_holds`,
77 `cost_selection_native_slim_holds`, or their tags.
78-/
79
80import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimality
81
82namespace IndisputableMonolith
83namespace Foundation
84namespace PrimitiveRecognitionCalculus
85namespace PRCJCost
86
87open scoped ArithmeticFunction.Omega
88
89/-! ## Part 1: the Liouville sign twist
90
91The two-point-anchor necessity witness. `liouvilleSign` reads the parity of
92the total prime-exponent count of the reduced fraction; the twist multiplies
93each display by that sign. -/
94
95/-- The Liouville-type sign of a rational display: `(-1)` to the total number
96of prime factors (with multiplicity) of numerator and denominator of the
97reduced fraction; Mathlib's `cardFactors` totalizes `Ω 0 = 0`, so the sign is
98`+1` at `0`. `-1` on every prime, `±1` everywhere. -/
99def liouvilleSign (t : ℚ) : ℚ :=
100 (-1) ^ (Ω t.num.natAbs + Ω t.den)
101
102/-- The twisted display `liouvilleSign t · t`. -/
103def liouvilleTwistDisplay (t : ℚ) : ℚ :=
104 liouvilleSign t * t
105
106theorem liouvilleSign_mul_self (t : ℚ) :
107 liouvilleSign t * liouvilleSign t = 1 := by
108 rw [liouvilleSign, ← pow_add, ← two_mul, pow_mul]
109 norm_num
110
111theorem liouvilleSign_ne_zero (t : ℚ) : liouvilleSign t ≠ 0 := by
112 rw [liouvilleSign]
113 positivity
114
115theorem liouvilleSign_one : liouvilleSign 1 = 1 := by
116 rw [liouvilleSign]
117 norm_num
118
119theorem liouvilleSign_neg_one : liouvilleSign (-1) = 1 := by
120 rw [liouvilleSign]
121 norm_num
122
123/-- The reduced-fraction cross identity for products: numerators and
124denominators of `t₁ * t₂` differ from the raw products only by a common
125cancelled factor. -/
126theorem rat_mul_num_den_cross (t₁ t₂ : ℚ) :
127 (t₁ * t₂).num * ((t₁.den : ℤ) * (t₂.den : ℤ)) =
128 t₁.num * t₂.num * ((t₁ * t₂).den : ℤ) := by
129 have h1 : ((t₁ * t₂).num : ℚ) = (t₁ * t₂) * (((t₁ * t₂).den : ℚ)) :=
130 (div_eq_iff (by exact_mod_cast (t₁ * t₂).den_ne_zero)).mp
131 (Rat.num_div_den (t₁ * t₂))
132 have h2 : (t₁.num : ℚ) = t₁ * ((t₁.den : ℚ)) :=
133 (div_eq_iff (by exact_mod_cast t₁.den_ne_zero)).mp (Rat.num_div_den t₁)
134 have h3 : (t₂.num : ℚ) = t₂ * ((t₂.den : ℚ)) :=
135 (div_eq_iff (by exact_mod_cast t₂.den_ne_zero)).mp (Rat.num_div_den t₂)
136 have key : ((t₁ * t₂).num : ℚ) * ((t₁.den : ℚ) * (t₂.den : ℚ)) =
137 (t₁.num : ℚ) * (t₂.num : ℚ) * (((t₁ * t₂).den : ℚ)) := by
138 rw [h1, h2, h3]
139 ring
140 exact_mod_cast key
141
142/-- Complete multiplicativity of the Liouville sign on nonzero rationals:
143cancellation removes the same factors from numerator and denominator, so the
144total parity is preserved. -/
145theorem liouvilleSign_mul {t₁ t₂ : ℚ} (h₁ : t₁ ≠ 0) (h₂ : t₂ ≠ 0) :
146 liouvilleSign (t₁ * t₂) = liouvilleSign t₁ * liouvilleSign t₂ := by
147 have hA : (t₁ * t₂).num.natAbs ≠ 0 :=
148 Int.natAbs_ne_zero.mpr (Rat.num_ne_zero.mpr (mul_ne_zero h₁ h₂))
149 have hn₁ : t₁.num.natAbs ≠ 0 :=
150 Int.natAbs_ne_zero.mpr (Rat.num_ne_zero.mpr h₁)
151 have hn₂ : t₂.num.natAbs ≠ 0 :=
152 Int.natAbs_ne_zero.mpr (Rat.num_ne_zero.mpr h₂)
153 have hd₁ : t₁.den ≠ 0 := t₁.den_ne_zero
154 have hd₂ : t₂.den ≠ 0 := t₂.den_ne_zero
155 have hD : (t₁ * t₂).den ≠ 0 := (t₁ * t₂).den_ne_zero
156 have hcross : (t₁ * t₂).num.natAbs * (t₁.den * t₂.den) =
157 t₁.num.natAbs * t₂.num.natAbs * (t₁ * t₂).den := by
158 have h := congrArg Int.natAbs (rat_mul_num_den_cross t₁ t₂)
159 simpa [Int.natAbs_mul] using h
160 have hexp : Ω (t₁ * t₂).num.natAbs + (Ω t₁.den + Ω t₂.den) =
161 (Ω t₁.num.natAbs + Ω t₂.num.natAbs) + Ω (t₁ * t₂).den := by
162 have hL : Ω ((t₁ * t₂).num.natAbs * (t₁.den * t₂.den)) =
163 Ω (t₁ * t₂).num.natAbs + (Ω t₁.den + Ω t₂.den) := by
164 rw [ArithmeticFunction.cardFactors_mul hA (mul_ne_zero hd₁ hd₂),
165 ArithmeticFunction.cardFactors_mul hd₁ hd₂]
166 have hR : Ω (t₁.num.natAbs * t₂.num.natAbs * (t₁ * t₂).den) =
167 (Ω t₁.num.natAbs + Ω t₂.num.natAbs) + Ω (t₁ * t₂).den := by
168 rw [ArithmeticFunction.cardFactors_mul (mul_ne_zero hn₁ hn₂) hD,
169 ArithmeticFunction.cardFactors_mul hn₁ hn₂]
170 rw [← hL, ← hR, hcross]
171 have hmod : (Ω (t₁ * t₂).num.natAbs + Ω (t₁ * t₂).den) % 2 =
172 (Ω t₁.num.natAbs + Ω t₁.den + (Ω t₂.num.natAbs + Ω t₂.den)) % 2 := by
173 omega
174 rw [liouvilleSign, liouvilleSign, liouvilleSign, ← pow_add,
175 neg_one_pow_eq_pow_mod_two, hmod, ← neg_one_pow_eq_pow_mod_two]
176
177theorem liouvilleSign_inv {t : ℚ} (h : t ≠ 0) :
178 liouvilleSign t⁻¹ = liouvilleSign t := by
179 have hmul := liouvilleSign_mul h (inv_ne_zero h)
180 rw [mul_inv_cancel₀ h, liouvilleSign_one] at hmul
181 calc liouvilleSign t⁻¹
182 = liouvilleSign t * liouvilleSign t * liouvilleSign t⁻¹ := by
183 rw [liouvilleSign_mul_self, one_mul]
184 _ = liouvilleSign t * (liouvilleSign t * liouvilleSign t⁻¹) := by ring
185 _ = liouvilleSign t := by rw [← hmul, mul_one]
186
187theorem liouvilleSign_natCast_prime {p : ℕ} (hp : p.Prime) :
188 liouvilleSign (p : ℚ) = -1 := by
189 rw [liouvilleSign, Rat.num_natCast, Rat.den_natCast, Int.natAbs_natCast,
190 ArithmeticFunction.cardFactors_apply_prime hp,
191 ArithmeticFunction.cardFactors_one]
192 norm_num
193
194/-! ### Twist-value lemmas -/
195
196theorem liouvilleTwistDisplay_zero : liouvilleTwistDisplay 0 = 0 := by
197 rw [liouvilleTwistDisplay, mul_zero]
198
199theorem liouvilleTwistDisplay_one : liouvilleTwistDisplay 1 = 1 := by
200 rw [liouvilleTwistDisplay, liouvilleSign_one, mul_one]
201
202theorem liouvilleTwistDisplay_neg_one : liouvilleTwistDisplay (-1) = -1 := by
203 rw [liouvilleTwistDisplay, liouvilleSign_neg_one, one_mul]
204
205theorem liouvilleTwistDisplay_two : liouvilleTwistDisplay 2 = -2 := by
206 have h2 : liouvilleSign (2 : ℚ) = -1 := by
207 have := liouvilleSign_natCast_prime (p := 2) Nat.prime_two
208 simpa using this
209 rw [liouvilleTwistDisplay, h2]
210 norm_num
211
212theorem liouvilleTwistDisplay_ne_zero {t : ℚ} (h : t ≠ 0) :
213 liouvilleTwistDisplay t ≠ 0 :=
214 mul_ne_zero (liouvilleSign_ne_zero t) h
215
216theorem liouvilleTwistDisplay_mul {t₁ t₂ : ℚ} (h₁ : t₁ ≠ 0) (h₂ : t₂ ≠ 0) :
217 liouvilleTwistDisplay (t₁ * t₂) =
218 liouvilleTwistDisplay t₁ * liouvilleTwistDisplay t₂ := by
219 rw [liouvilleTwistDisplay, liouvilleTwistDisplay, liouvilleTwistDisplay,
220 liouvilleSign_mul h₁ h₂]
221 ring
222
223theorem liouvilleTwistDisplay_inv (t : ℚ) :
224 liouvilleTwistDisplay t⁻¹ = (liouvilleTwistDisplay t)⁻¹ := by
225 by_cases h : t = 0
226 · rw [h]
227 simp [liouvilleTwistDisplay_zero]
228 · rw [liouvilleTwistDisplay, liouvilleTwistDisplay, liouvilleSign_inv h,
229 mul_inv]
230 have hs := liouvilleSign_mul_self t
231 have hne := liouvilleSign_ne_zero t
232 have hinv : (liouvilleSign t)⁻¹ = liouvilleSign t := by
233 field_simp
234 nlinarith [hs]
235 rw [hinv]
236
237/-- Signs cancel on products of two primes (including `p = r`). -/
238theorem liouvilleTwistDisplay_prime_pair {p r : ℕ}
239 (hp : p.Prime) (hr : r.Prime) :
240 liouvilleTwistDisplay ((p : ℚ) * (r : ℚ)) = (p : ℚ) * (r : ℚ) := by
241 have hp0 : (p : ℚ) ≠ 0 := by exact_mod_cast hp.ne_zero
242 have hr0 : (r : ℚ) ≠ 0 := by exact_mod_cast hr.ne_zero
243 rw [liouvilleTwistDisplay, liouvilleSign_mul hp0 hr0,
244 liouvilleSign_natCast_prime hp, liouvilleSign_natCast_prime hr]
245 ring
246
247/-! ### The Liouville-twisted native cost -/
248
249/-- The Liouville-twisted native cost: displays `J(liouvilleSign t · t)` on
250every orbit, with the unit display sent to the literal zero representative
251(the standard exact-unit wrapper). -/
252def liouvilleTwistNativeCost (q : RatioOrbit) : RatioOrbit :=
253 if q.toRat = 1 then RatioOrbit.zero
254 else onRatioOrbit (ratioOrbitOfRat (liouvilleTwistDisplay q.toRat))
255
256theorem liouvilleTwistNativeCost_toRat (q : RatioOrbit) :
257 (liouvilleTwistNativeCost q).toRat =
258 (liouvilleTwistDisplay q.toRat +
259 (liouvilleTwistDisplay q.toRat)⁻¹) / 2 - 1 := by
260 rw [liouvilleTwistNativeCost]
261 by_cases h : q.toRat = 1
262 · rw [if_pos h, RatioOrbit.zero_toRat, h, liouvilleTwistDisplay_one]
263 norm_num
264 · rw [if_neg h, onRatioOrbit_toRat, ratioOrbitOfRat_toRat]
265
266/-! ## Part 2: the sans-two-calibration class and its refutation -/
267
268/-- The base native-cost fields WITHOUT the two-point anchor. -/
269structure PRCNativeCostHypothesesSansTwoCalibration
270 (F : RatioOrbit → RatioOrbit) : Prop where
271 reciprocal :
272 ∀ q, RatioOrbit.crossEq (F q) (F (RatioOrbit.recip q))
273 normalized_invariant :
274 ∀ q, RatioOrbit.crossEq (F q) (F (DistinctionNat.normalizeRatio q))
275 canonical_rcl :
276 ∀ {x y : RatioOrbit}, x.toRat ≠ 0 → y.toRat ≠ 0 →
277 RatioOrbit.crossEq
278 (RatioOrbit.add (F (RatioOrbit.mul x y)) (F (div x y)))
279 (RatioOrbit.add
280 (RatioOrbit.add
281 (RatioOrbit.mul two (RatioOrbit.mul (F x) (F y)))
282 (RatioOrbit.mul two (F x)))
283 (RatioOrbit.mul two (F y)))
284 unit_zero :
285 F RatioOrbit.one = RatioOrbit.zero
286
287/-- Slim ledger minus the two-point anchor: base-sans-two + pairs + sign +
288zero. -/
289structure PRCSlimSansTwoCalibrationHypotheses
290 (F : RatioOrbit → RatioOrbit) : Prop where
291 base_sans_two : PRCNativeCostHypothesesSansTwoCalibration F
292 prime_pair_product_cost : PRCNativeCostPrimePairProductCalibrated F
293 signed_unit : PRCNativeCostSignedUnitCalibrated F
294 zero_calibrated :
295 PRCDoubledTraceZeroCalibrated (nativeCostDoubledTrace F)
296
297/-- Uniqueness target for the sans-two-calibration class. -/
298def PRCSlimSansTwoCalibrationUniquenessTarget : Prop :=
299 ∀ F : RatioOrbit → RatioOrbit,
300 PRCSlimSansTwoCalibrationHypotheses F →
301 ∀ q : RatioOrbit,
302 RatioOrbit.crossEq (F q) (onRatioOrbit q)
303
304/-- Bridging iff: the slim ledger is exactly the sans-two class plus the
305two-point anchor, so the refutation below is a necessity statement about the
306slim ledger's own field. -/
307theorem slim_iff_sansTwo_and_two_calibrated (F : RatioOrbit → RatioOrbit) :
308 PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses F ↔
309 (PRCSlimSansTwoCalibrationHypotheses F ∧
310 RatioOrbit.crossEq (F two) (onRatioOrbit two)) := by
311 constructor
312 · intro h
313 exact ⟨⟨⟨h.signed_strengthened.strengthened.native.reciprocal,
314 h.signed_strengthened.strengthened.native.normalized_invariant,
315 h.signed_strengthened.strengthened.native.canonical_rcl,
316 h.signed_strengthened.strengthened.native.unit_zero⟩,
317 h.signed_strengthened.strengthened.prime_pair_product_cost,
318 h.signed_strengthened.signed_unit,
319 h.zero_calibrated⟩,
320 h.signed_strengthened.strengthened.native.two_calibrated⟩
321 · rintro ⟨h, htwo⟩
322 exact ⟨⟨⟨⟨h.base_sans_two.reciprocal, h.base_sans_two.normalized_invariant,
323 h.base_sans_two.canonical_rcl, h.base_sans_two.unit_zero, htwo⟩,
324 h.prime_pair_product_cost⟩, h.signed_unit⟩, h.zero_calibrated⟩
325
326/-- Non-vacuity of the sans-two class: the canonical witness inhabits it. -/
327theorem canonicalSelectedNativeCost_sans_two_hypotheses :
328 PRCSlimSansTwoCalibrationHypotheses canonicalSelectedNativeCost :=
329 ((slim_iff_sansTwo_and_two_calibrated canonicalSelectedNativeCost).mp
330 canonicalSelectedNativeCost_slim_hypotheses).1
331
332/-- The Liouville twist satisfies every slim field except the two-point
333anchor. -/
334theorem liouvilleTwistNativeCost_sans_two_hypotheses :
335 PRCSlimSansTwoCalibrationHypotheses liouvilleTwistNativeCost where
336 base_sans_two :=
337 { reciprocal := by
338 intro q
339 rw [RatioOrbit.crossEq_iff_toRat_eq, liouvilleTwistNativeCost_toRat,
340 liouvilleTwistNativeCost_toRat, RatioOrbit.recip_toRat,
341 liouvilleTwistDisplay_inv, inv_inv]
342 ring
343 normalized_invariant := by
344 intro q
345 rw [RatioOrbit.crossEq_iff_toRat_eq, liouvilleTwistNativeCost_toRat,
346 liouvilleTwistNativeCost_toRat, DistinctionNat.normalizeRatio_toRat]
347 canonical_rcl := by
348 intro x y hx hy
349 rw [RatioOrbit.crossEq_iff_toRat_eq]
350 simp only [RatioOrbit.add_toRat, RatioOrbit.mul_toRat,
351 liouvilleTwistNativeCost_toRat, div_toRat, two_toRat]
352 have hdiv : x.toRat / y.toRat = x.toRat * y.toRat⁻¹ :=
353 div_eq_mul_inv _ _
354 rw [liouvilleTwistDisplay_mul hx hy, hdiv,
355 liouvilleTwistDisplay_mul hx (inv_ne_zero hy),
356 liouvilleTwistDisplay_inv]
357 have ha : liouvilleTwistDisplay x.toRat ≠ 0 :=
358 liouvilleTwistDisplay_ne_zero hx
359 have hb : liouvilleTwistDisplay y.toRat ≠ 0 :=
360 liouvilleTwistDisplay_ne_zero hy
361 field_simp
362 ring
363 unit_zero := by
364 rw [liouvilleTwistNativeCost, if_pos RatioOrbit.one_toRat] }
365 prime_pair_product_cost := by
366 intro p hp r hr
367 rw [RatioOrbit.crossEq_iff_toRat_eq, liouvilleTwistNativeCost_toRat,
368 onRatioOrbit_toRat, RatioOrbit.mul_toRat, primeDirection_toRat,
369 primeDirection_toRat,
370 liouvilleTwistDisplay_prime_pair (natPrime_toNat_of_primeOrbit hp)
371 (natPrime_toNat_of_primeOrbit hr)]
372 signed_unit := by
373 rw [PRCNativeCostSignedUnitCalibrated, RatioOrbit.crossEq_iff_toRat_eq,
374 liouvilleTwistNativeCost_toRat, onRatioOrbit_toRat,
375 negativeOneRatio_toRat, liouvilleTwistDisplay_neg_one]
376 zero_calibrated := by
377 rw [PRCDoubledTraceZeroCalibrated, RatioOrbit.crossEq_iff_toRat_eq]
378 simp only [nativeCostDoubledTrace, doubledTraceValue, RatioOrbit.mul_toRat,
379 RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat,
380 liouvilleTwistNativeCost_toRat, RatioOrbit.zero_toRat,
381 liouvilleTwistDisplay_zero]
382 norm_num
383
384/-- The Liouville twist fails the two-point anchor: it displays `J(-2) = -9/4`
385at orbit 2 against the canonical `J(2) = 1/4`. -/
386theorem liouvilleTwistNativeCost_two_not_canonical :
387 ¬ RatioOrbit.crossEq (liouvilleTwistNativeCost two) (onRatioOrbit two) := by
388 rw [RatioOrbit.crossEq_iff_toRat_eq, liouvilleTwistNativeCost_toRat,
389 onRatioOrbit_toRat, two_toRat, liouvilleTwistDisplay_two]
390 norm_num
391
392/-- **Two-point-anchor necessity.** Slim minus two-calibration admits the
393Liouville twist, so the anchor cannot be dropped. -/
394theorem PRCSlimSansTwoCalibrationUniquenessTarget_refuted :
395 ¬ PRCSlimSansTwoCalibrationUniquenessTarget := by
396 intro huniq
397 exact liouvilleTwistNativeCost_two_not_canonical
398 (huniq liouvilleTwistNativeCost
399 liouvilleTwistNativeCost_sans_two_hypotheses two)
400
401/-! ## Part 3: the sans-pair class and its refutation -/
402
403/-- Slim ledger minus prime-pair products: full base + sign + zero. -/
404structure PRCSlimSansPairHypotheses
405 (F : RatioOrbit → RatioOrbit) : Prop where
406 native : PRCNativeCostHypotheses F
407 signed_unit : PRCNativeCostSignedUnitCalibrated F
408 zero_calibrated :
409 PRCDoubledTraceZeroCalibrated (nativeCostDoubledTrace F)
410
411/-- Uniqueness target for the sans-pair class. -/
412def PRCSlimSansPairUniquenessTarget : Prop :=
413 ∀ F : RatioOrbit → RatioOrbit,
414 PRCSlimSansPairHypotheses F →
415 ∀ q : RatioOrbit,
416 RatioOrbit.crossEq (F q) (onRatioOrbit q)
417
418/-- Bridging iff for the pair field. -/
419theorem slim_iff_sansPair_and_pair_calibrated (F : RatioOrbit → RatioOrbit) :
420 PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses F ↔
421 (PRCSlimSansPairHypotheses F ∧
422 PRCNativeCostPrimePairProductCalibrated F) := by
423 constructor
424 · intro h
425 exact ⟨⟨h.signed_strengthened.strengthened.native,
426 h.signed_strengthened.signed_unit, h.zero_calibrated⟩,
427 h.signed_strengthened.strengthened.prime_pair_product_cost⟩
428 · rintro ⟨h, hpair⟩
429 exact ⟨⟨⟨h.native, hpair⟩, h.signed_unit⟩, h.zero_calibrated⟩
430
431/-- Non-vacuity of the sans-pair class. -/
432theorem canonicalSelectedNativeCost_sans_pair_hypotheses :
433 PRCSlimSansPairHypotheses canonicalSelectedNativeCost :=
434 ((slim_iff_sansPair_and_pair_calibrated canonicalSelectedNativeCost).mp
435 canonicalSelectedNativeCost_slim_hypotheses).1
436
437/-- The two-adic twist fixes the display `0` (its numerator kills the
438product). -/
439theorem twoAdicTwistRat_zero : twoAdicTwistRat 0 = 0 := by
440 unfold twoAdicTwistRat
441 exact zero_mul _
442
443/-- The two-adic twist fixes the signed unit: `-1` has zero 2-adic
444valuation. -/
445theorem twoAdicTwistRat_neg_one : twoAdicTwistRat (-1) = -1 := by
446 unfold twoAdicTwistRat
447 have h : padicValRat 2 (-1 : ℚ) = 0 := by
448 rw [padicValRat.neg]
449 norm_num [padicValRat.of_int, padicValInt.eq_zero_of_not_dvd]
450 rw [h]
451 norm_num
452
453/-- The two-adic axis-twist cost calibrates the signed unit. -/
454theorem twoAdicGeneratedNativeCost_signed_unit :
455 PRCNativeCostSignedUnitCalibrated twoAdicGeneratedNativeCost := by
456 rw [PRCNativeCostSignedUnitCalibrated]
457 refine RatioOrbit.crossEq_trans
458 (twoAdicGeneratedNativeCost_crossEq_generated negativeOneRatio) ?_
459 rw [RatioOrbit.crossEq_iff_toRat_eq, costFromCharacter_toRat,
460 twoAdicAxisTwistCharacter_toRat, onRatioOrbit_toRat,
461 negativeOneRatio_toRat, twoAdicTwistRat_neg_one]
462
463/-- The two-adic axis-twist cost calibrates the zero orbit. -/
464theorem twoAdicGeneratedNativeCost_zero_calibrated :
465 PRCDoubledTraceZeroCalibrated
466 (nativeCostDoubledTrace twoAdicGeneratedNativeCost) := by
467 rw [PRCDoubledTraceZeroCalibrated, RatioOrbit.crossEq_iff_toRat_eq]
468 have hgen := twoAdicGeneratedNativeCost_crossEq_generated RatioOrbit.zero
469 rw [RatioOrbit.crossEq_iff_toRat_eq, costFromCharacter_toRat,
470 twoAdicAxisTwistCharacter_toRat, RatioOrbit.zero_toRat,
471 twoAdicTwistRat_zero] at hgen
472 simp only [nativeCostDoubledTrace, doubledTraceValue, RatioOrbit.mul_toRat,
473 RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat,
474 RatioOrbit.zero_toRat, hgen]
475 norm_num
476
477/-- The two-adic twist inhabits the sans-pair class. -/
478theorem twoAdicGeneratedNativeCost_sans_pair_hypotheses :
479 PRCSlimSansPairHypotheses twoAdicGeneratedNativeCost where
480 native := twoAdicGeneratedNativeCost_hypotheses
481 signed_unit := twoAdicGeneratedNativeCost_signed_unit
482 zero_calibrated := twoAdicGeneratedNativeCost_zero_calibrated
483
484/-- **Pair-field necessity.** Base + sign + zero admit the two-adic twist,
485which the parent module proves fails prime-pair products at the mixed (2,3)
486orbit; the pair field cannot be dropped. -/
487theorem PRCSlimSansPairUniquenessTarget_refuted :
488 ¬ PRCSlimSansPairUniquenessTarget := by
489 intro huniq
490 apply twoAdicGeneratedNativeCost_not_prime_pair_product_calibrated
491 intro p hp r hr
492 exact huniq twoAdicGeneratedNativeCost
493 twoAdicGeneratedNativeCost_sans_pair_hypotheses
494 (RatioOrbit.mul (primeDirection p hp) (primeDirection r hr))
495
496/-! ## Part 4: the sans-sign class and its refutation -/
497
498/-- Slim ledger minus the signed unit: strengthened (base + pairs) + zero. -/
499structure PRCSlimSansSignHypotheses
500 (F : RatioOrbit → RatioOrbit) : Prop where
501 strengthened : PRCStrengthenedNativeCostHypotheses F
502 zero_calibrated :
503 PRCDoubledTraceZeroCalibrated (nativeCostDoubledTrace F)
504
505/-- Uniqueness target for the sans-sign class. -/
506def PRCSlimSansSignUniquenessTarget : Prop :=
507 ∀ F : RatioOrbit → RatioOrbit,
508 PRCSlimSansSignHypotheses F →
509 ∀ q : RatioOrbit,
510 RatioOrbit.crossEq (F q) (onRatioOrbit q)
511
512/-- Bridging iff for the signed-unit field. -/
513theorem slim_iff_sansSign_and_signed_unit (F : RatioOrbit → RatioOrbit) :
514 PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses F ↔
515 (PRCSlimSansSignHypotheses F ∧
516 PRCNativeCostSignedUnitCalibrated F) := by
517 constructor
518 · intro h
519 exact ⟨⟨h.signed_strengthened.strengthened, h.zero_calibrated⟩,
520 h.signed_strengthened.signed_unit⟩
521 · rintro ⟨h, hsign⟩
522 exact ⟨⟨h.strengthened, hsign⟩, h.zero_calibrated⟩
523
524/-- Non-vacuity of the sans-sign class. -/
525theorem canonicalSelectedNativeCost_sans_sign_hypotheses :
526 PRCSlimSansSignHypotheses canonicalSelectedNativeCost :=
527 ((slim_iff_sansSign_and_signed_unit canonicalSelectedNativeCost).mp
528 canonicalSelectedNativeCost_slim_hypotheses).1
529
530/-- The absolute-value cost inhabits the sans-sign class (all fields already
531proved in the parent module). -/
532theorem absValueGeneratedNativeCost_sans_sign_hypotheses :
533 PRCSlimSansSignHypotheses absValueGeneratedNativeCost where
534 strengthened := absValueGeneratedNativeCost_strengthened_hypotheses
535 zero_calibrated := absValueGeneratedNativeCost_doubled_trace_zero_calibrated
536
537/-- **Signed-unit necessity.** Base + pairs + zero admit the absolute-value
538cost, which the parent module proves fails at the signed unit; the sign field
539cannot be dropped. -/
540theorem PRCSlimSansSignUniquenessTarget_refuted :
541 ¬ PRCSlimSansSignUniquenessTarget := by
542 intro huniq
543 exact absValueGeneratedNativeCost_negative_one_not_canonical
544 (huniq absValueGeneratedNativeCost
545 absValueGeneratedNativeCost_sans_sign_hypotheses negativeOneRatio)
546
547/-! ## Part 5: the sans-zero class (round-2 reuse)
548
549Slim minus the zero-orbit field IS `PRCSignedStrengthenedNativeCostHypotheses`
550verbatim, and its uniqueness target was refuted in round 2 by the zero-flat
551witness. Only the bridging iff is new. -/
552
553/-- Bridging iff for the zero-orbit field (definitional). -/
554theorem slim_iff_sansZero_and_zero_calibrated (F : RatioOrbit → RatioOrbit) :
555 PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses F ↔
556 (PRCSignedStrengthenedNativeCostHypotheses F ∧
557 PRCDoubledTraceZeroCalibrated (nativeCostDoubledTrace F)) :=
558 ⟨fun h => ⟨h.signed_strengthened, h.zero_calibrated⟩,
559 fun h => ⟨h.1, h.2⟩⟩
560
561/-- Non-vacuity of the sans-zero class. -/
562theorem canonicalSelectedNativeCost_sans_zero_hypotheses :
563 PRCSignedStrengthenedNativeCostHypotheses canonicalSelectedNativeCost :=
564 canonicalSelectedNativeCost_slim_hypotheses.signed_strengthened
565
566/-! ## Part 5b (preregistered bonus): the RCL core is necessary
567
568The prereg allowed one bonus beyond the four removable calibration fields:
569necessity of the nonzero RCL itself, witnessed by a spike at an orbit no
570retained field can reach. Orbit `5` qualifies: the calibration probes are
571`2` (two-point anchor), products of two primes (never a prime), `-1`, `0`,
572and `1`, and the reciprocity/normalization fields only move a spike between
573`5` and `1/5`. The spiked cost (canonical J displays everywhere except the
574`5`- and `1/5`-displays, which are sent to `0`) inhabits "slim minus RCL"
575and differs from J at `5`. This does NOT extend to the remaining structural
576fields (reciprocity, normalization invariance, unit-zero), whose necessity
577stays OPEN. The frozen certificate structure below keeps its preregistered
578shape; this section is a separate deposit. -/
579
580/-- The base native-cost fields WITHOUT the nonzero RCL. -/
581structure PRCNativeCostHypothesesSansRcl
582 (F : RatioOrbit → RatioOrbit) : Prop where
583 reciprocal :
584 ∀ q, RatioOrbit.crossEq (F q) (F (RatioOrbit.recip q))
585 normalized_invariant :
586 ∀ q, RatioOrbit.crossEq (F q) (F (DistinctionNat.normalizeRatio q))
587 unit_zero :
588 F RatioOrbit.one = RatioOrbit.zero
589 two_calibrated :
590 RatioOrbit.crossEq (F two) (onRatioOrbit two)
591
592/-- Slim ledger minus the nonzero RCL. -/
593structure PRCSlimSansRclHypotheses
594 (F : RatioOrbit → RatioOrbit) : Prop where
595 base_sans_rcl : PRCNativeCostHypothesesSansRcl F
596 prime_pair_product_cost : PRCNativeCostPrimePairProductCalibrated F
597 signed_unit : PRCNativeCostSignedUnitCalibrated F
598 zero_calibrated :
599 PRCDoubledTraceZeroCalibrated (nativeCostDoubledTrace F)
600
601/-- Uniqueness target for the sans-RCL class. -/
602def PRCSlimSansRclUniquenessTarget : Prop :=
603 ∀ F : RatioOrbit → RatioOrbit,
604 PRCSlimSansRclHypotheses F →
605 ∀ q : RatioOrbit,
606 RatioOrbit.crossEq (F q) (onRatioOrbit q)
607
608/-- Bridging iff for the RCL field (explicit binders on the RCL component). -/
609theorem slim_iff_sansRcl_and_rcl (F : RatioOrbit → RatioOrbit) :
610 PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses F ↔
611 (PRCSlimSansRclHypotheses F ∧
612 (∀ x y : RatioOrbit, x.toRat ≠ 0 → y.toRat ≠ 0 →
613 RatioOrbit.crossEq
614 (RatioOrbit.add (F (RatioOrbit.mul x y)) (F (div x y)))
615 (RatioOrbit.add
616 (RatioOrbit.add
617 (RatioOrbit.mul two (RatioOrbit.mul (F x) (F y)))
618 (RatioOrbit.mul two (F x)))
619 (RatioOrbit.mul two (F y))))) := by
620 constructor
621 · intro h
622 exact ⟨⟨⟨h.signed_strengthened.strengthened.native.reciprocal,
623 h.signed_strengthened.strengthened.native.normalized_invariant,
624 h.signed_strengthened.strengthened.native.unit_zero,
625 h.signed_strengthened.strengthened.native.two_calibrated⟩,
626 h.signed_strengthened.strengthened.prime_pair_product_cost,
627 h.signed_strengthened.signed_unit,
628 h.zero_calibrated⟩,
629 fun _ _ hx hy =>
630 h.signed_strengthened.strengthened.native.canonical_rcl hx hy⟩
631 · rintro ⟨h, hrcl⟩
632 exact ⟨⟨⟨⟨h.base_sans_rcl.reciprocal,
633 h.base_sans_rcl.normalized_invariant,
634 fun {x y} hx hy => hrcl x y hx hy,
635 h.base_sans_rcl.unit_zero,
636 h.base_sans_rcl.two_calibrated⟩,
637 h.prime_pair_product_cost⟩, h.signed_unit⟩, h.zero_calibrated⟩
638
639/-- Non-vacuity of the sans-RCL class. -/
640theorem canonicalSelectedNativeCost_sans_rcl_hypotheses :
641 PRCSlimSansRclHypotheses canonicalSelectedNativeCost :=
642 ((slim_iff_sansRcl_and_rcl canonicalSelectedNativeCost).mp
643 canonicalSelectedNativeCost_slim_hypotheses).1
644
645/-- The RCL-spike witness: canonical J displays everywhere except the `5`-
646and `1/5`-displays, which are sent to the zero representative. -/
647def rclSpikeNativeCost (q : RatioOrbit) : RatioOrbit :=
648 if q.toRat = 5 ∨ q.toRat = 5⁻¹ then RatioOrbit.zero
649 else canonicalSelectedNativeCost q
650
651theorem rclSpikeNativeCost_toRat (q : RatioOrbit) :
652 (rclSpikeNativeCost q).toRat =
653 if q.toRat = 5 ∨ q.toRat = 5⁻¹ then 0
654 else (q.toRat + q.toRat⁻¹) / 2 - 1 := by
655 rw [rclSpikeNativeCost]
656 split_ifs with h
657 · exact RatioOrbit.zero_toRat
658 · exact canonicalSelectedNativeCost_toRat q
659
660/-- The spike set is closed under display inversion. -/
661theorem rclSpike_inv_iff (t : ℚ) :
662 (t⁻¹ = 5 ∨ t⁻¹ = 5⁻¹) ↔ (t = 5 ∨ t = 5⁻¹) := by
663 constructor
664 · rintro (h | h)
665 · right
666 rw [inv_eq_iff_eq_inv] at h
667 exact h
668 · left
669 exact inv_inj.mp (by rw [h])
670 · rintro (h | h)
671 · right
672 rw [h]
673 · left
674 rw [h, inv_inv]
675
676theorem rclSpikeNativeCost_sans_rcl_hypotheses :
677 PRCSlimSansRclHypotheses rclSpikeNativeCost where
678 base_sans_rcl :=
679 { reciprocal := by
680 intro q
681 rw [RatioOrbit.crossEq_iff_toRat_eq, rclSpikeNativeCost_toRat,
682 rclSpikeNativeCost_toRat, RatioOrbit.recip_toRat]
683 by_cases h : q.toRat = 5 ∨ q.toRat = 5⁻¹
684 · rw [if_pos h, if_pos ((rclSpike_inv_iff q.toRat).mpr h)]
685 · rw [if_neg h, if_neg (fun hc => h ((rclSpike_inv_iff q.toRat).mp hc))]
686 by_cases hq : q.toRat = 0
687 · rw [hq]
688 norm_num
689 · field_simp
690 ring
691 normalized_invariant := by
692 intro q
693 rw [RatioOrbit.crossEq_iff_toRat_eq, rclSpikeNativeCost_toRat,
694 rclSpikeNativeCost_toRat, DistinctionNat.normalizeRatio_toRat]
695 unit_zero := by
696 rw [rclSpikeNativeCost,
697 if_neg (by rw [RatioOrbit.one_toRat]; norm_num)]
698 exact canonicalSelectedNativeCost_native_hypotheses.unit_zero
699 two_calibrated := by
700 have h : rclSpikeNativeCost two = canonicalSelectedNativeCost two := by
701 rw [rclSpikeNativeCost, if_neg (by rw [two_toRat]; norm_num)]
702 rw [h]
703 exact canonicalSelectedNativeCost_native_hypotheses.two_calibrated }
704 prime_pair_product_cost := by
705 intro p hp r hr
706 have hpP : Nat.Prime p.toNat := natPrime_toNat_of_primeOrbit hp
707 have hrP : Nat.Prime r.toNat := natPrime_toNat_of_primeOrbit hr
708 have hnospike :
709 ¬ ((RatioOrbit.mul (primeDirection p hp)
710 (primeDirection r hr)).toRat = 5 ∨
711 (RatioOrbit.mul (primeDirection p hp)
712 (primeDirection r hr)).toRat = 5⁻¹) := by
713 rw [RatioOrbit.mul_toRat, primeDirection_toRat, primeDirection_toRat]
714 rintro (h | h)
715 · have hnat : p.toNat * r.toNat = 5 := by exact_mod_cast h
716 have h5 : Nat.Prime 5 := by norm_num
717 rcases (h5.eq_one_or_self_of_dvd p.toNat ⟨r.toNat, hnat.symm⟩) with
718 h1 | h5p
719 · exact hpP.one_lt.ne' h1
720 · rw [h5p] at hnat
721 have : r.toNat = 1 := by omega
722 exact hrP.one_lt.ne' this
723 · have hnat : p.toNat * r.toNat * 5 = 1 := by
724 have h1 : ((p.toNat : ℚ) * (r.toNat : ℚ)) * 5 = 1 := by
725 rw [h]
726 norm_num
727 exact_mod_cast h1
728 omega
729 have heq :
730 rclSpikeNativeCost
731 (RatioOrbit.mul (primeDirection p hp) (primeDirection r hr)) =
732 canonicalSelectedNativeCost
733 (RatioOrbit.mul (primeDirection p hp) (primeDirection r hr)) := by
734 rw [rclSpikeNativeCost, if_neg hnospike]
735 rw [heq]
736 exact canonicalSelectedNativeCost_crossEq_onRatioOrbit _
737 signed_unit := by
738 rw [PRCNativeCostSignedUnitCalibrated]
739 have h : rclSpikeNativeCost negativeOneRatio =
740 canonicalSelectedNativeCost negativeOneRatio := by
741 rw [rclSpikeNativeCost,
742 if_neg (by rw [negativeOneRatio_toRat]; norm_num)]
743 rw [h]
744 exact canonicalSelectedNativeCost_crossEq_onRatioOrbit negativeOneRatio
745 zero_calibrated := by
746 have h : rclSpikeNativeCost RatioOrbit.zero =
747 canonicalSelectedNativeCost RatioOrbit.zero := by
748 rw [rclSpikeNativeCost,
749 if_neg (by rw [RatioOrbit.zero_toRat]; norm_num)]
750 rw [PRCDoubledTraceZeroCalibrated, nativeCostDoubledTrace, h]
751 exact canonicalSelectedNativeCost_full_hypotheses.zero_calibrated
752
753/-- The spike differs from the canonical cost at the `5`-display orbit. -/
754theorem rclSpikeNativeCost_five_not_canonical :
755 ¬ RatioOrbit.crossEq (rclSpikeNativeCost (ratioOrbitOfRat 5))
756 (onRatioOrbit (ratioOrbitOfRat 5)) := by
757 rw [RatioOrbit.crossEq_iff_toRat_eq, rclSpikeNativeCost_toRat,
758 onRatioOrbit_toRat, ratioOrbitOfRat_toRat,
759 if_pos (Or.inl rfl)]
760 norm_num
761
762/-- **RCL-core necessity (bonus).** Slim minus the nonzero RCL admits the
763`5`-spike, so the RCL field cannot be dropped either. -/
764theorem PRCSlimSansRclUniquenessTarget_refuted :
765 ¬ PRCSlimSansRclUniquenessTarget := by
766 intro huniq
767 exact rclSpikeNativeCost_five_not_canonical
768 (huniq rclSpikeNativeCost rclSpikeNativeCost_sans_rcl_hypotheses
769 (ratioOrbitOfRat 5))
770
771/-! ## Part 6: the certificate -/
772
773/-- **Field-by-field minimality certificate for the slim ledger.** The slim
774ledger forces the canonical J-cost (round 2), and each of its four removable
775calibration fields is necessary: dropping any one admits a kernel-checked
776impostor (Liouville twist, two-adic twist, absolute-value cost, zero-flat
777cost respectively). -/
778structure SlimLedgerMinimalityCertificate : Prop where
779 slim_uniqueness :
780 PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget
781 two_point_anchor_necessary :
782 ¬ PRCSlimSansTwoCalibrationUniquenessTarget
783 pair_field_necessary :
784 ¬ PRCSlimSansPairUniquenessTarget
785 signed_unit_necessary :
786 ¬ PRCSlimSansSignUniquenessTarget
787 zero_orbit_necessary :
788 ¬ PRCSignedStrengthenedNativeCostUniquenessTarget
789
790theorem slimLedgerMinimalityCertificate_holds :
791 SlimLedgerMinimalityCertificate where
792 slim_uniqueness :=
793 PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved
794 two_point_anchor_necessary :=
795 PRCSlimSansTwoCalibrationUniquenessTarget_refuted
796 pair_field_necessary :=
797 PRCSlimSansPairUniquenessTarget_refuted
798 signed_unit_necessary :=
799 PRCSlimSansSignUniquenessTarget_refuted
800 zero_orbit_necessary :=
801 PRCSignedStrengthenedNativeCostUniquenessTarget_refuted
802
803/-- The certificate deposit. `deltaOnly`: all cost domains and codomains are
804`RatioOrbit` and all display arithmetic is discrete; the witnesses are
805arithmetically explicit (some parent wrappers use eliminable classical
806equality tests), and no completed carrier, continuum object, or continuity
807premise appears in any statement or witness (see the header for the
808deliberation against the wall convention). -/
809theorem slim_ledger_minimality_certificate_tagged :
810 PublicSpine.Tagged StrengthTag.deltaOnly SlimLedgerMinimalityCertificate
811 where
812 holds := slimLedgerMinimalityCertificate_holds
813
814/-! ## Axiom audit (standard basis only) -/
815
816#print axioms slimLedgerMinimalityCertificate_holds
817#print axioms slim_ledger_minimality_certificate_tagged
818#print axioms PRCSlimSansTwoCalibrationUniquenessTarget_refuted
819#print axioms PRCSlimSansPairUniquenessTarget_refuted
820#print axioms PRCSlimSansSignUniquenessTarget_refuted
821#print axioms slim_iff_sansTwo_and_two_calibrated
822#print axioms slim_iff_sansPair_and_pair_calibrated
823#print axioms slim_iff_sansSign_and_signed_unit
824#print axioms slim_iff_sansZero_and_zero_calibrated
825#print axioms PRCSlimSansRclUniquenessTarget_refuted
826#print axioms slim_iff_sansRcl_and_rcl
827
828end PRCJCost
829end PrimitiveRecognitionCalculus
830end Foundation
831end IndisputableMonolith
832