IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimality
IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostMinimality.lean · 517 lines · 19 declarations
show as:
view math explainer →
1/-
2 PrimitiveRecognitionCalculus/PRCNativeCostMinimality.lean
3
4 Round-trip source:
5 δ/plans/JCost_AllPrime_CostLevel_Minimality_Prereg_20260724.json (frozen)
6 plans/Delta_JCost_AllPrime_CostLevel_Minimality_Session_Prompt_20260724.txt
7
8 Cost-level minimality of the all-prime calibration family (P-delta-jfree,
9 round 2). The round-1 mint (`PRCNativeCostSelection.lean`) deposited
10 `CostSelectionPackageNative` at `deltaOnly` over a ledger whose largest item
11 is calibration on EVERY native prime axis, and left OPEN whether that
12 countable family is necessary at the cost level. This module settles it:
13
14 * REDUNDANT. `PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget`
15 is proved: the slim ledger (base + prime-pair products + signed unit +
16 zero orbit, WITHOUT the all-prime field) already forces the canonical
17 cost. The new mathematical content is
18 `character_pair_two_calibration_forces_prime_calibration`: for a ratio
19 character, prime-pair product cost consistency plus the base ledger's
20 single two-point calibration force cost calibration on every prime axis.
21 The dichotomies J(x)=J(y) ⟺ y ∈ {x, 1/x} at the orbits 2, 2p, p·p leave
22 exactly the identity and reciprocal branches; every mixed branch dies on
23 integer arithmetic (16·P⁴ = 1 or 16 = 1 with P ≥ 1).
24
25 * The launch prompt's named target
26 `PRCSignedStrengthenedNativeCostUniquenessTarget` (slim ledger WITHOUT the
27 zero field) is REFUTED: the round-1 zero-flat witness satisfies the
28 STRONGER prime-signed ledger, hence also this weaker one, and differs
29 from the canonical cost at the zero orbit. This is the uninteresting
30 refutation: it says only that the zero orbit stays invisible to the
31 nonzero RCL.
32
33 * `cost_selection_native_slim_holds` mints the contracted deposit at
34 `deltaOnly`: uniqueness over the slim ledger, non-vacuity, the frozen
35 decoy exclusions, and the layer-discrimination pair for the zero-flat
36 cost (passes the slim ledger minus zero, fails the slim ledger).
37
38 Honest reading: the round-1 deposit's ledger was honest but fat. After the
39 zero-orbit calibration supplies the character factorization, the orbit-2
40 anchor together with the (2,p) and (p,p) pair probes forces every
41 prime-axis cost calibration; the signed unit plays no role in this
42 transport step. What remains genuinely open, with countermodel sketches
43 recorded in the prereg: cost-level necessity of the two-point calibration
44 itself relative to pairs+sign+zero (paper-level countermodel: the
45 Liouville-type sign twist χ(q) = λ(q)·q, which passes pairs because signs
46 cancel on products of two primes; within the slim ledger it fails exactly
47 the two-point calibration, while against the round-1 full ledger it also
48 fails every prime-axis field), and a formalized necessity witness for the
49 pair field relative to base+sign+zero.
50
51 Scope: reads `PRCNativeCostSelection.lean` (round-1 witnesses and decoys)
52 and through it `PRCNativeCostUniqueness.lean`. It edits neither, and never
53 touches `cost_selection_holds`, `cost_selection_native_holds`, or their
54 tags.
55-/
56
57import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostSelection
58
59namespace IndisputableMonolith
60namespace Foundation
61namespace PrimitiveRecognitionCalculus
62namespace PRCJCost
63
64/-! ## The named launch target, settled: REFUTED by inclusion
65
66The signed-strengthened ledger carries no zero-orbit field, so the round-1
67zero-flat witness (which satisfies the STRONGER prime-signed ledger, hence
68also this weaker one) already defeats it. -/
69
70/-- **The launch prompt's named target is refuted.** The signed-strengthened
71ledger (base + pairs + signed unit, no zero field) admits the zero-flat
72countermodel: every one of its fields lives on nonzero orbits. -/
73theorem PRCSignedStrengthenedNativeCostUniquenessTarget_refuted :
74 ¬ PRCSignedStrengthenedNativeCostUniquenessTarget := by
75 intro h
76 have hzero :=
77 h zeroFlatNativeCost
78 zeroFlatNativeCost_prime_signed_strengthened_hypotheses.signed_strengthened
79 RatioOrbit.zero
80 rw [zeroFlatNativeCost_zero, RatioOrbit.crossEq_iff_toRat_eq,
81 RatioOrbit.zero_toRat, onRatioOrbit_toRat, RatioOrbit.zero_toRat] at hzero
82 norm_num at hzero
83
84/-- Corollary: the signed-strengthened ledger cannot factor every inhabitant
85through a signed-admissible character (the zero-flat cost cannot factor, since
86character-generated costs are canonical at the zero orbit). -/
87theorem PRCSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget_refuted :
88 ¬ PRCSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget :=
89 fun h =>
90 PRCSignedStrengthenedNativeCostUniquenessTarget_refuted
91 (PRCSignedStrengthenedNativeCostUniquenessTarget_of_signed_admissible_factorization
92 h)
93
94/-! ## The core new lemma: pairs + the two-point calibration force every axis
95
96Pure rational case analysis behind the transport. `u` is the character value
97at the two axis, `v` at the probed prime axis, `P ≥ 1` the prime display. -/
98
99private lemma pair_two_case_split {u v P : ℚ} (hP : P ≠ 0) (hP1 : 1 ≤ P)
100 (hu : u = 2 ∨ u = 2⁻¹)
101 (huv : u * v = 2 * P ∨ u * v = (2 * P)⁻¹)
102 (hvv : v * v = P * P ∨ v * v = (P * P)⁻¹) :
103 v = P ∨ v = P⁻¹ := by
104 have hpow : (1:ℚ) ≤ P ^ 4 := one_le_pow₀ hP1
105 have h2P : (2:ℚ) * P ≠ 0 := mul_ne_zero (by norm_num) hP
106 have hPP : P * P ≠ 0 := mul_ne_zero hP hP
107 rcases hu with hu | hu
108 · subst hu
109 rcases huv with huv | huv
110 · left
111 linarith
112 · exfalso
113 have h1 : 4 * P * v = 1 := by
114 linear_combination (2 * P) * huv + mul_inv_cancel₀ h2P
115 rcases hvv with hvv | hvv
116 · have h16 : (16:ℚ) * P ^ 4 = 1 := by
117 linear_combination (4 * P * v + 1) * h1 - 16 * P ^ 2 * hvv
118 linarith
119 · have hvvP : v * v * (P * P) = 1 := by
120 rw [hvv]
121 exact inv_mul_cancel₀ hPP
122 have h15 : (15:ℚ) = 0 := by
123 linear_combination (4 * P * v + 1) * h1 - 16 * hvvP
124 norm_num at h15
125 · subst hu
126 rcases huv with huv | huv
127 · exfalso
128 have h1 : v = 4 * P := by
129 linear_combination 2 * huv
130 rcases hvv with hvv | hvv
131 · have h15 : (15:ℚ) * P ^ 2 = 0 := by
132 linear_combination hvv - (v + 4 * P) * h1
133 have hpos : (0:ℚ) < P ^ 2 := by positivity
134 nlinarith
135 · have hvvP : v * v * (P * P) = 1 := by
136 rw [hvv]
137 exact inv_mul_cancel₀ hPP
138 have h16 : (16:ℚ) * P ^ 4 = 1 := by
139 linear_combination hvvP - (v * P ^ 2 + 4 * P ^ 3) * h1
140 linarith
141 · right
142 have h1 : v * P = 1 := by
143 linear_combination 2 * P * huv + mul_inv_cancel₀ h2P
144 field_simp
145 linear_combination h1
146
147/-- **Prime-pair products plus the base two-point calibration force cost
148calibration on every native prime axis.** This is the transport the round-1
149premise ledger was missing: the all-prime family is not independent data once
150the pair field and the base ledger's two-calibration are present. -/
151theorem character_pair_two_calibration_forces_prime_calibration
152 {χ : RatioOrbit → RatioOrbit}
153 (hχ : PRCRatioCharacter χ)
154 (hpair : PRCCharacterPrimePairProductCostConsistent χ)
155 (htwo : RatioOrbit.crossEq (costFromCharacter χ two) (onRatioOrbit two)) :
156 PRCCharacterPrimeDirectionCalibrated χ := by
157 intro p hp
158 -- displays
159 have hPne : (primeDirection p hp).toRat ≠ 0 := primeDirection_toRat_ne_zero p hp
160 have hvne : (χ (primeDirection p hp)).toRat ≠ 0 := hχ.nonzero_preserving hPne
161 have hPnat : p.toNat ≠ 0 := by
162 have h := hPne
163 rw [primeDirection_toRat] at h
164 exact_mod_cast h
165 have hP1 : (1:ℚ) ≤ (p.toNat : ℚ) := by
166 exact_mod_cast Nat.one_le_iff_ne_zero.mpr hPnat
167 have hPQ : ((p.toNat : ℚ)) ≠ 0 := by
168 rw [← primeDirection_toRat p hp]
169 exact hPne
170 have hpd2Rat : (primeDirection twoOrbit twoOrbit_primeOrbit).toRat = 2 := by
171 rw [primeDirection_toRat, twoOrbit_toNat]
172 norm_num
173 -- the character respects crossEq (native GCD normalization is canonical)
174 have hrespect : PRCCharacterRespectsCrossEq χ :=
175 PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical hχ
176 PRCNormalizeRatioCanonicalTarget_proved
177 -- transfer the two-point calibration to the two prime direction
178 have h2cross :
179 RatioOrbit.crossEq two (primeDirection twoOrbit twoOrbit_primeOrbit) := by
180 rw [RatioOrbit.crossEq_iff_toRat_eq, two_toRat, hpd2Rat]
181 have hχtwoEq :
182 (χ two).toRat = (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat := by
183 have h := hrespect two (primeDirection twoOrbit twoOrbit_primeOrbit) h2cross
184 rw [RatioOrbit.crossEq_iff_toRat_eq] at h
185 exact h
186 -- dichotomy at the two orbit
187 have h2ne : (two : RatioOrbit).toRat ≠ 0 := by
188 rw [two_toRat]
189 norm_num
190 have hχ2ne : (χ two).toRat ≠ 0 := hχ.nonzero_preserving h2ne
191 have hu :
192 (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat = 2 ∨
193 (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat = 2⁻¹ := by
194 rcases jcost_eq_forces_same_or_reciprocal hχ2ne h2ne
195 (by simpa [costFromCharacter] using htwo) with h | h
196 · left
197 rw [RatioOrbit.crossEq_iff_toRat_eq, two_toRat] at h
198 rw [← hχtwoEq]
199 exact h
200 · right
201 rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.recip_toRat, two_toRat] at h
202 rw [← hχtwoEq]
203 exact h
204 -- dichotomy at the pair (2, p)
205 have h2pne :
206 (RatioOrbit.mul (primeDirection twoOrbit twoOrbit_primeOrbit)
207 (primeDirection p hp)).toRat ≠ 0 := by
208 rw [RatioOrbit.mul_toRat, hpd2Rat]
209 exact mul_ne_zero (by norm_num) hPne
210 have hmul2p :
211 (χ (RatioOrbit.mul (primeDirection twoOrbit twoOrbit_primeOrbit)
212 (primeDirection p hp))).toRat =
213 (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat *
214 (χ (primeDirection p hp)).toRat := by
215 have h := hχ.multiplicative (primeDirection twoOrbit twoOrbit_primeOrbit)
216 (primeDirection p hp)
217 rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.mul_toRat] at h
218 exact h
219 have huv :
220 (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat *
221 (χ (primeDirection p hp)).toRat =
222 2 * (p.toNat : ℚ) ∨
223 (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat *
224 (χ (primeDirection p hp)).toRat =
225 (2 * (p.toNat : ℚ))⁻¹ := by
226 have hχ2pne :
227 (χ (RatioOrbit.mul (primeDirection twoOrbit twoOrbit_primeOrbit)
228 (primeDirection p hp))).toRat ≠ 0 :=
229 hχ.nonzero_preserving h2pne
230 rcases jcost_eq_forces_same_or_reciprocal hχ2pne h2pne
231 (by simpa [costFromCharacter]
232 using hpair twoOrbit twoOrbit_primeOrbit p hp) with h | h
233 · left
234 rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.mul_toRat, hpd2Rat,
235 primeDirection_toRat] at h
236 rw [← hmul2p]
237 exact h
238 · right
239 rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.recip_toRat,
240 RatioOrbit.mul_toRat, hpd2Rat, primeDirection_toRat] at h
241 rw [← hmul2p]
242 exact h
243 -- dichotomy at the pair (p, p)
244 have hppne :
245 (RatioOrbit.mul (primeDirection p hp) (primeDirection p hp)).toRat ≠ 0 := by
246 rw [RatioOrbit.mul_toRat]
247 exact mul_ne_zero hPne hPne
248 have hmulpp :
249 (χ (RatioOrbit.mul (primeDirection p hp) (primeDirection p hp))).toRat =
250 (χ (primeDirection p hp)).toRat * (χ (primeDirection p hp)).toRat := by
251 have h := hχ.multiplicative (primeDirection p hp) (primeDirection p hp)
252 rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.mul_toRat] at h
253 exact h
254 have hvv :
255 (χ (primeDirection p hp)).toRat * (χ (primeDirection p hp)).toRat =
256 (p.toNat : ℚ) * (p.toNat : ℚ) ∨
257 (χ (primeDirection p hp)).toRat * (χ (primeDirection p hp)).toRat =
258 ((p.toNat : ℚ) * (p.toNat : ℚ))⁻¹ := by
259 have hχppne :
260 (χ (RatioOrbit.mul (primeDirection p hp) (primeDirection p hp))).toRat ≠
261 0 :=
262 hχ.nonzero_preserving hppne
263 rcases jcost_eq_forces_same_or_reciprocal hχppne hppne
264 (by simpa [costFromCharacter] using hpair p hp p hp) with h | h
265 · left
266 rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.mul_toRat,
267 primeDirection_toRat] at h
268 rw [← hmulpp]
269 exact h
270 · right
271 rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.recip_toRat,
272 RatioOrbit.mul_toRat, primeDirection_toRat] at h
273 rw [← hmulpp]
274 exact h
275 -- the case split leaves the identity or reciprocal branch
276 have hbranch :
277 (χ (primeDirection p hp)).toRat = (p.toNat : ℚ) ∨
278 (χ (primeDirection p hp)).toRat = ((p.toNat : ℚ))⁻¹ :=
279 pair_two_case_split hPQ hP1 hu huv hvv
280 -- both branches carry the same J display
281 rw [RatioOrbit.crossEq_iff_toRat_eq, costFromCharacter_toRat, onRatioOrbit_toRat,
282 primeDirection_toRat]
283 rcases hbranch with h | h
284 · rw [h]
285 · rw [h, inv_inv]
286 ring
287
288/-! ## The slim ledger and its uniqueness theorem -/
289
290/-- The slim hypothesis class: the round-1 minted ledger WITHOUT the all-prime
291axis field. Base (reciprocity, normalization invariance, nonzero RCL,
292unit-zero, two-calibration) + prime-pair products + signed unit + zero orbit. -/
293structure PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses
294 (F : RatioOrbit → RatioOrbit) : Prop where
295 signed_strengthened : PRCSignedStrengthenedNativeCostHypotheses F
296 zero_calibrated :
297 PRCDoubledTraceZeroCalibrated (nativeCostDoubledTrace F)
298
299/-- Uniqueness over the slim ledger. -/
300def PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget : Prop :=
301 ∀ F : RatioOrbit → RatioOrbit,
302 PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses F →
303 ∀ q : RatioOrbit,
304 RatioOrbit.crossEq (F q) (onRatioOrbit q)
305
306/-- **The slim ledger already forces J.** Factorization needs only base + zero;
307the pair and sign fields transfer to the factor character; the new transport
308lemma recovers per-prime calibration from the pair field and the base
309two-calibration; the existing signed-admissible rigidity closes. -/
310theorem PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved :
311 PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget := by
312 intro F hF q
313 rcases PRCZeroCalibratedNativeCostCharacterFactorizationTarget_proved F
314 hF.signed_strengthened.strengthened.native hF.zero_calibrated with
315 ⟨χ, hχ, hFχ⟩
316 have hpair : PRCCharacterPrimePairProductCostConsistent χ := by
317 intro p hp r hr
318 exact RatioOrbit.crossEq_trans
319 (RatioOrbit.crossEq_symm
320 (hFχ (RatioOrbit.mul (primeDirection p hp) (primeDirection r hr))))
321 (hF.signed_strengthened.strengthened.prime_pair_product_cost p hp r hr)
322 have htwoCal :
323 RatioOrbit.crossEq (costFromCharacter χ two) (onRatioOrbit two) :=
324 RatioOrbit.crossEq_trans (RatioOrbit.crossEq_symm (hFχ two))
325 hF.signed_strengthened.strengthened.native.two_calibrated
326 have hprime : PRCCharacterPrimeDirectionCalibrated χ :=
327 character_pair_two_calibration_forces_prime_calibration hχ hpair htwoCal
328 have hsignCost :
329 RatioOrbit.crossEq (costFromCharacter χ negativeOneRatio)
330 (onRatioOrbit negativeOneRatio) :=
331 RatioOrbit.crossEq_trans (RatioOrbit.crossEq_symm (hFχ negativeOneRatio))
332 hF.signed_strengthened.signed_unit
333 have hsign : PRCCharacterSignedUnitCalibrated χ :=
334 costFromCharacter_negativeOne_forces_signed_unit hχ hsignCost
335 exact RatioOrbit.crossEq_trans (hFχ q)
336 (PRCNativeCostSignedAdmissibleCharacterRigidityTarget_proved χ
337 ⟨⟨hχ, hprime, hpair⟩, hsign⟩ q)
338
339/-! ## The ledger contraction, stated -/
340
341/-- **The all-prime axis field is redundant.** Every inhabitant of the slim
342ledger is automatically calibrated on every native prime axis. -/
343theorem all_prime_axis_field_redundant
344 (F : RatioOrbit → RatioOrbit)
345 (hF : PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses F) :
346 PRCNativeCostPrimeDirectionCalibrated F := fun p hp =>
347 PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved
348 F hF (primeDirection p hp)
349
350/-- The slim ledger and the round-1 minted ledger carve out the same class of
351native costs. -/
352theorem slim_class_iff_full_class (F : RatioOrbit → RatioOrbit) :
353 PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses F ↔
354 PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses F := by
355 constructor
356 · intro hF
357 exact
358 { prime_signed :=
359 { signed_strengthened := hF.signed_strengthened
360 prime_direction_cost := all_prime_axis_field_redundant F hF }
361 zero_calibrated := hF.zero_calibrated }
362 · intro hF
363 exact
364 { signed_strengthened := hF.prime_signed.signed_strengthened
365 zero_calibrated := hF.zero_calibrated }
366
367/-! ## Witness and decoys against the slim class -/
368
369/-- The round-1 non-vacuity witness inhabits the slim class. -/
370theorem canonicalSelectedNativeCost_slim_hypotheses :
371 PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses
372 canonicalSelectedNativeCost :=
373 (slim_class_iff_full_class canonicalSelectedNativeCost).mpr
374 canonicalSelectedNativeCost_full_hypotheses
375
376/-- Decoy exclusion 1 against the slim class (dies at the base
377two-calibration). -/
378theorem constantZeroNativeCost_slim_excluded :
379 ¬ PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses
380 constantZeroNativeCost :=
381 fun h =>
382 constantZeroNativeCost_not_native_hypotheses
383 h.signed_strengthened.strengthened.native
384
385/-- Decoy exclusion 2 against the slim class (dies at the base
386two-calibration). -/
387theorem linearNativeCost_slim_excluded :
388 ¬ PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses linearNativeCost :=
389 fun h =>
390 linearNativeCost_not_native_hypotheses
391 h.signed_strengthened.strengthened.native
392
393/-- Layer discrimination: the zero-flat cost passes every slim field except
394the zero orbit (round-1 theorem gives it the larger prime-signed class), and
395fails the slim class exactly there. -/
396theorem zeroFlatNativeCost_slim_excluded :
397 ¬ PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses
398 zeroFlatNativeCost := by
399 intro h
400 have hz := h.zero_calibrated
401 rw [PRCDoubledTraceZeroCalibrated, RatioOrbit.crossEq_iff_toRat_eq] at hz
402 simp only [nativeCostDoubledTrace, doubledTraceValue, zeroFlatNativeCost_zero,
403 RatioOrbit.mul_toRat, RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat,
404 RatioOrbit.zero_toRat] at hz
405 norm_num at hz
406
407/-! ## The contracted deposit -/
408
409/-- **The slim native cost-selection package** (prereg
410PREREG-jfree-minimality-20260724). The round-1 package with the all-prime
411axis field deleted from the ledger:
412
413* `j_unique_native_slim`: every native cost satisfying base + prime-pair
414 products + signed unit + zero orbit is crossEq-pointwise the canonical
415 cost.
416* `non_vacuous`: the round-1 witness inhabits the slim class.
417* `zero_cost_excluded` / `linear_cost_excluded`: the frozen known-wrong costs
418 fail the slim class.
419* `zero_flat_passes_without_zero` / `zero_flat_excluded`: the
420 layer-discrimination pair; the slim class's zero field is doing real work.
421
422Same honest reading as round 1 (conditional δ-native rigidity, statement on
423the countable carrier, classical proof shell disclosed by the axiom audit),
424with one item less to pay for: the calibration ledger is now finite data on
425the generators 2 and -1, the pair products, and the zero orbit. -/
426structure CostSelectionPackageNativeSlim : Prop where
427 j_unique_native_slim :
428 PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget
429 non_vacuous :
430 ∃ F : RatioOrbit → RatioOrbit,
431 PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses F ∧
432 ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (onRatioOrbit q)
433 zero_cost_excluded :
434 ¬ PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses
435 constantZeroNativeCost
436 linear_cost_excluded :
437 ¬ PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses linearNativeCost
438 zero_flat_passes_without_zero :
439 PRCSignedStrengthenedNativeCostHypotheses zeroFlatNativeCost
440 zero_flat_excluded :
441 ¬ PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses zeroFlatNativeCost
442
443/-- The slim package holds. -/
444theorem costSelectionPackageNativeSlim_holds : CostSelectionPackageNativeSlim where
445 j_unique_native_slim :=
446 PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved
447 non_vacuous :=
448 ⟨canonicalSelectedNativeCost, canonicalSelectedNativeCost_slim_hypotheses,
449 canonicalSelectedNativeCost_crossEq_onRatioOrbit⟩
450 zero_cost_excluded := constantZeroNativeCost_slim_excluded
451 linear_cost_excluded := linearNativeCost_slim_excluded
452 zero_flat_passes_without_zero :=
453 zeroFlatNativeCost_prime_signed_strengthened_hypotheses.signed_strengthened
454 zero_flat_excluded := zeroFlatNativeCost_slim_excluded
455
456/-- **The contracted deposit.** Same grade as round 1 (`deltaOnly`, statement
457on the countable carrier under the PublicSpine statement-carrier convention),
458with the all-prime calibration family removed from the price. -/
459theorem cost_selection_native_slim_holds :
460 PublicSpine.Tagged StrengthTag.deltaOnly CostSelectionPackageNativeSlim where
461 holds := costSelectionPackageNativeSlim_holds
462
463/-! ## The contracted premise ledger
464
465Round 1's `nativeCostSelectionPremiseLedger` listed five items and left the
466all-prime item's cost-level minimality OPEN. This session closes that item:
467it is DERIVABLE, so the contracted ledger has four. -/
468
469/-- The contracted premise ledger for the slim deposit. -/
470def nativeCostSelectionSlimPremiseLedger : List StrengthClaim :=
471 [ { label := "base"
472 tag := StrengthTag.deltaOnly
473 statement := "Reciprocity, normalization invariance, canonical RCL on \
474nonzero orbits, unit-zero, two-calibration (PRCNativeCostHypotheses). \
475Necessity: PRCNativeCostUniquenessTarget_refuted (two-adic axis twist)." }
476 , { label := "prime_pair_products"
477 tag := StrengthTag.deltaOnly
478 statement := "Calibration on products of two prime directions \
479(PRCNativeCostPrimePairProductCalibrated). Necessity: the two-adic generated \
480cost slips through the base ledger exactly on such products." }
481 , { label := "signed_unit"
482 tag := StrengthTag.deltaOnly
483 statement := "Calibration at the signed unit -1 \
484(PRCNativeCostSignedUnitCalibrated). Necessity: \
485PRCStrengthenedNativeCostUniquenessTarget_refuted (absolute-value cost)." }
486 , { label := "zero_orbit"
487 tag := StrengthTag.deltaOnly
488 statement := "Zero-orbit calibration of the doubled trace \
489(PRCDoubledTraceZeroCalibrated). Necessity: \
490PRCSignedStrengthenedNativeCostUniquenessTarget_refuted (zero-flat \
491countermodel, this module); the nonzero RCL never sees the zero orbit." }
492 ]
493
494/-- The contracted ledger stays at the δ-only floor. -/
495theorem nativeCostSelectionSlimPremiseLedger_all_deltaOnly :
496 ∀ c ∈ nativeCostSelectionSlimPremiseLedger,
497 c.tag = StrengthTag.deltaOnly := by
498 intro c hc
499 simp only [nativeCostSelectionSlimPremiseLedger, List.mem_cons,
500 List.not_mem_nil, or_false] at hc
501 rcases hc with h | h | h | h <;> subst h <;> rfl
502
503/-! ## Axiom audit (headline receipts) -/
504
505#print axioms PRCSignedStrengthenedNativeCostUniquenessTarget_refuted
506#print axioms character_pair_two_calibration_forces_prime_calibration
507#print axioms PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved
508#print axioms all_prime_axis_field_redundant
509#print axioms slim_class_iff_full_class
510#print axioms costSelectionPackageNativeSlim_holds
511#print axioms cost_selection_native_slim_holds
512
513end PRCJCost
514end PrimitiveRecognitionCalculus
515end Foundation
516end IndisputableMonolith
517