IndisputableMonolith.Foundation.ScaleHomogeneityNoGo
IndisputableMonolith/Foundation/ScaleHomogeneityNoGo.lean · 362 lines · 31 declarations
show as:
view math explainer →
1import Mathlib
2
3/-!
4 ScaleHomogeneityNoGo.lean
5
6 The boundary theorem of the forced skeleton, in neutral vocabulary.
7
8 The uniqueness chain (T-2 through T8) derives the skeleton of the theory
9 without a scale. This module proves, once and abstractly, why the chain
10 cannot go further on its own: no selection criterion that is blind to
11 joint rescaling of a posted value and its carrier can fix an absolute
12 value for a scale-invariant target. Any such criterion that accepts the
13 intended witness also accepts a doubled decoy whose posted value misses
14 the target. Hence at least one scale-bearing input is required.
15
16 The statement is deliberately type-agnostic: the carrier `X` is any type
17 equipped with a positive-real scaling action. Two witnesses built from
18 ordinary mathematical types (real pairs with a squared ratio, and
19 eight-component complex vectors with a probability weight) instantiate
20 the hypotheses, so the no-go is a general fact about scale-invariant
21 selection, not a property of any particular carrier.
22
23 This is the canonical public form of the boundary theorem used in the
24 paper "Recognition Composition and the Forced Skeleton". The ledger
25 instantiation (`MassGenesis.T10JointScaleHomogeneityNoGo`) lives in the
26 full Recognition Science library and is an instance of the class theorem
27 proved here.
28
29 The module carries the theorem in two forms. `ScaleHomogeneityNoGo`
30 proves the joint-selector form (a posted value against a
31 scale-invariant target). `ScaleHomogeneityNoGo.AmplitudeForm` proves
32 the paper's S5 statement verbatim: over a scaled configuration space
33 (a `ℝ_{>0}`-action with a degree-one homogeneous amplitude), an
34 invariant selector's selected amplitude set is contained in `{0}` or
35 contains every positive real, with the positive-quadrant witness
36 pinning the scale-invariant ratio `a/b` to `2` while leaving the
37 amplitude free.
38
39 No `sorry`; no new Lean `axiom`.
40-/
41
42namespace IndisputableMonolith
43namespace Foundation
44
45universe u
46
47/-- A positive-real scaling action on a carrier `X`. The action laws are
48recorded so that instances cannot smuggle in state-dependent rescaling. -/
49structure ScaleAction (X : Type u) where
50 scale : ℝ → X → X
51 scale_one : ∀ x, scale 1 x = x
52 scale_mul : ∀ c d x, scale (c * d) x = scale c (scale d x)
53
54namespace ScaleHomogeneityNoGo
55
56noncomputable section
57
58variable {X : Type u} (act : ScaleAction X)
59
60/-- A candidate selector is invariant under joint positive rescaling of the
61posted value and the carrier. -/
62def IsJointScaleInvariantSelector (S : ℝ → X → Prop) : Prop :=
63 ∀ (c : ℝ), 0 < c → ∀ (a : ℝ) (x : X), S a x ↔ S (c * a) (act.scale c x)
64
65/-- A target functional is scale-invariant when rescaling the carrier does
66not change its value. -/
67def IsScaleInvariant (f : X → ℝ) : Prop :=
68 ∀ (c : ℝ), 0 < c → ∀ x, f (act.scale c x) = f x
69
70/-- Main class theorem (the doubling decoy): no joint-scale-invariant
71selector that accepts the intended witness can force the posted value to
72the scale-invariant target. Proof: from `S (f x₀) x₀` joint invariance
73gives `S (2 * f x₀) (scale 2 x₀)`, and scale invariance of `f` gives
74`f (scale 2 x₀) = f x₀ ≠ 2 * f x₀`. -/
75theorem no_scaleInvariantSelector_forces_value
76 (S : ℝ → X → Prop) (hS : IsJointScaleInvariantSelector act S)
77 (f : X → ℝ) (hf : IsScaleInvariant act f)
78 (x₀ : X) (hpos : 0 < f x₀) (h₀ : S (f x₀) x₀) :
79 ¬ ∀ (a : ℝ) (x : X), S a x → a = f x := by
80 intro hall
81 have h2 : S (2 * f x₀) (act.scale 2 x₀) :=
82 (hS 2 (by norm_num) (f x₀) x₀).mp h₀
83 have hfx : f (act.scale 2 x₀) = f x₀ := hf 2 (by norm_num) x₀
84 have heq := hall _ _ h2
85 rw [hfx] at heq
86 linarith [hpos]
87
88/-- Admission-gate export: any selector that does force the posted value on
89the intended witness cannot be joint-scale invariant. -/
90theorem forcingSelector_not_jointScaleInvariant
91 (S : ℝ → X → Prop) (f : X → ℝ) (hf : IsScaleInvariant act f)
92 (x₀ : X) (hpos : 0 < f x₀) (h₀ : S (f x₀) x₀)
93 (hforces : ∀ (a : ℝ) (x : X), S a x → a = f x) :
94 ¬ IsJointScaleInvariantSelector act S := by
95 intro hS
96 exact no_scaleInvariantSelector_forces_value act S hS f hf x₀ hpos h₀ hforces
97
98/-- The positivity selector: accepts exactly the positive posted values.
99It ignores the carrier, so it is joint-scale invariant for any action. -/
100def PositivitySelector : ℝ → X → Prop := fun a _ => 0 < a
101
102theorem positivitySelector_jointScaleInvariant :
103 IsJointScaleInvariantSelector act (PositivitySelector (X := X)) := by
104 intro c hc a x
105 constructor
106 · exact mul_pos hc
107 · exact fun h => pos_of_mul_pos_right h (le_of_lt hc)
108
109/-- Non-vacuity: the positivity selector lies in the class, accepts the
110intended witness whenever the target is positive there, and therefore
111cannot force the target value. -/
112theorem positivitySelector_does_not_force_value
113 (f : X → ℝ) (hf : IsScaleInvariant act f)
114 (x₀ : X) (hpos : 0 < f x₀) :
115 ¬ ∀ (a : ℝ) (x : X), PositivitySelector a x → a = f x :=
116 no_scaleInvariantSelector_forces_value act _
117 (positivitySelector_jointScaleInvariant act) f hf x₀ hpos hpos
118
119/-- Certificate bundling the class wall, the admission export, and the
120non-vacuity witness. -/
121structure ScaleHomogeneityNoGoCert (X : Type u) (act : ScaleAction X) : Prop where
122 class_wall :
123 ∀ (S : ℝ → X → Prop), IsJointScaleInvariantSelector act S →
124 ∀ (f : X → ℝ), IsScaleInvariant act f →
125 ∀ (x₀ : X), 0 < f x₀ → S (f x₀) x₀ →
126 ¬ ∀ (a : ℝ) (x : X), S a x → a = f x
127 admission_export :
128 ∀ (S : ℝ → X → Prop) (f : X → ℝ), IsScaleInvariant act f →
129 ∀ (x₀ : X), 0 < f x₀ → S (f x₀) x₀ →
130 (∀ (a : ℝ) (x : X), S a x → a = f x) →
131 ¬ IsJointScaleInvariantSelector act S
132 class_nonempty : ∃ S, IsJointScaleInvariantSelector act S
133 class_inhabited_nonvacuous : Nonempty X →
134 ∃ (S : ℝ → X → Prop) (f : X → ℝ) (x₀ : X),
135 IsJointScaleInvariantSelector act S ∧ IsScaleInvariant act f ∧
136 0 < f x₀ ∧ S (f x₀) x₀
137
138theorem scaleHomogeneityNoGoCert (act : ScaleAction X) :
139 ScaleHomogeneityNoGoCert X act where
140 class_wall := fun S hS f hf x₀ hpos h₀ =>
141 no_scaleInvariantSelector_forces_value act S hS f hf x₀ hpos h₀
142 admission_export := fun S f hf x₀ hpos h₀ hforces =>
143 forcingSelector_not_jointScaleInvariant act S f hf x₀ hpos h₀ hforces
144 class_nonempty := ⟨PositivitySelector, positivitySelector_jointScaleInvariant act⟩
145 class_inhabited_nonvacuous := fun ⟨x₀⟩ =>
146 ⟨PositivitySelector, fun _ => 1, x₀,
147 positivitySelector_jointScaleInvariant act,
148 fun _c _hc _x => rfl, one_pos, one_pos⟩
149
150/-! ## Witness 1: real pairs with the squared ratio -/
151
152/-- Componentwise scaling of real pairs. -/
153def pairScaleAction : ScaleAction (ℝ × ℝ) where
154 scale c p := (c * p.1, c * p.2)
155 scale_one _ := by ext <;> simp
156 scale_mul _ _ _ := by ext <;> simp [mul_assoc]
157
158/-- The squared first-component share: invariant under joint scaling. -/
159def pairRatio (p : ℝ × ℝ) : ℝ := p.1 ^ 2 / (p.1 ^ 2 + p.2 ^ 2)
160
161theorem pairRatio_scaleInvariant : IsScaleInvariant pairScaleAction pairRatio := by
162 intro c hc p
163 show (c * p.1) ^ 2 / ((c * p.1) ^ 2 + (c * p.2) ^ 2) = _
164 rw [show (c * p.1) ^ 2 + (c * p.2) ^ 2 = c ^ 2 * (p.1 ^ 2 + p.2 ^ 2) by ring,
165 show (c * p.1) ^ 2 = c ^ 2 * p.1 ^ 2 by ring]
166 exact mul_div_mul_left _ _ (pow_ne_zero 2 (ne_of_gt hc))
167
168/-- The no-go instantiated on real pairs: no scale-blind criterion can
169recover the squared ratio as an absolute posted value. -/
170theorem pair_witness :
171 ¬ ∀ (a : ℝ) (p : ℝ × ℝ), PositivitySelector a p → a = pairRatio p := by
172 have hpos : 0 < pairRatio (1, 1) := by norm_num [pairRatio]
173 exact no_scaleInvariantSelector_forces_value pairScaleAction _
174 (positivitySelector_jointScaleInvariant pairScaleAction)
175 pairRatio pairRatio_scaleInvariant _ hpos hpos
176
177/-! ## Witness 2: eight-component complex vectors with a probability weight -/
178
179/-- Pointwise complex scaling of eight-component vectors. -/
180def vecScaleAction : ScaleAction (Fin 8 → ℂ) where
181 scale c ψ := fun i => (c : ℂ) * ψ i
182 scale_one _ := by funext i; simp
183 scale_mul _ _ _ := by funext i; push_cast; ring
184
185/-- The probability weight of the first component: invariant under joint
186scaling. -/
187def probWeight (ψ : Fin 8 → ℂ) : ℝ :=
188 ‖ψ 0‖ ^ 2 / ∑ i : Fin 8, ‖ψ i‖ ^ 2
189
190theorem probWeight_scaleInvariant : IsScaleInvariant vecScaleAction probWeight := by
191 intro c hc ψ
192 have hn : ∀ i : Fin 8, ‖(c : ℂ) * ψ i‖ = c * ‖ψ i‖ := fun i => by
193 rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos hc]
194 show ‖(c : ℂ) * ψ 0‖ ^ 2 / (∑ i : Fin 8, ‖(c : ℂ) * ψ i‖ ^ 2) = _
195 rw [show (∑ i : Fin 8, ‖(c : ℂ) * ψ i‖ ^ 2) = c ^ 2 * ∑ i : Fin 8, ‖ψ i‖ ^ 2 by
196 rw [Finset.mul_sum]
197 exact Finset.sum_congr rfl fun i _ => by rw [hn i]; ring]
198 rw [show ‖(c : ℂ) * ψ 0‖ ^ 2 = c ^ 2 * ‖ψ 0‖ ^ 2 by rw [hn 0]; ring]
199 exact mul_div_mul_left _ _ (pow_ne_zero 2 (ne_of_gt hc))
200
201/-- The no-go instantiated on eight-component complex vectors: no scale-blind
202criterion can recover an absolute normalization from a probability
203profile. -/
204theorem vec_witness :
205 ¬ ∀ (a : ℝ) (ψ : Fin 8 → ℂ), PositivitySelector a ψ → a = probWeight ψ := by
206 have hpos : 0 < probWeight (fun _ => (1 : ℂ)) := by
207 simp only [probWeight, norm_one, one_pow, Finset.sum_const, Finset.card_univ,
208 Fintype.card_fin, nsmul_eq_mul]
209 norm_num
210 exact no_scaleInvariantSelector_forces_value vecScaleAction _
211 (positivitySelector_jointScaleInvariant vecScaleAction)
212 probWeight probWeight_scaleInvariant _ hpos hpos
213
214end
215
216/-! ## The amplitude form (the paper's S5 statement)
217
218The capstone paper states the no-go in amplitude form: a scaled
219configuration space is a type carrying an action of the multiplicative
220group of positive reals and a degree-one homogeneous amplitude readout,
221and an invariant selector is a predicate blind to the action. The
222selected amplitude set is then either contained in `0` or contains every
223positive real, so no positive amplitude is forced unless the selector is
224unsatisfiable. The witness is the positive quadrant with `A(a,b) = a`
225and the selector `a = 2b`, which pins the scale-invariant ratio `a/b`
226to `2` while leaving the amplitude completely free: dimensionless
227readouts are outside the theorem's reach. This section is that form,
228kernel-checked, with its witness. -/
229
230namespace AmplitudeForm
231
232/-- A scaled configuration space: a carrier with a multiplicative
233`ℝ_{>0}`-action and a nonnegative amplitude readout, homogeneous of
234degree one. -/
235structure ScaledConfigSpace where
236 X : Type u
237 scale : {c : ℝ // 0 < c} → X → X
238 scale_one : ∀ x, scale ⟨1, one_pos⟩ x = x
239 scale_mul : ∀ (c d : {c : ℝ // 0 < c}) (x : X),
240 scale ⟨c.1 * d.1, mul_pos c.2 d.2⟩ x = scale c (scale d x)
241 A : X → ℝ
242 A_nonneg : ∀ x, 0 ≤ A x
243 A_homog : ∀ (c : {c : ℝ // 0 < c}) (x : X), A (scale c x) = c.1 * A x
244
245namespace ScaledConfigSpace
246
247variable (sp : ScaledConfigSpace)
248
249/-- A selector is invariant when it cannot distinguish a configuration
250from its rescaled copy. -/
251def IsInvariantSelector (P : sp.X → Prop) : Prop :=
252 ∀ (c : {c : ℝ // 0 < c}) (x : sp.X), P (sp.scale c x) ↔ P x
253
254/-- The scale-homogeneity no-go, amplitude form: the selected amplitude
255set is either contained in `{0}` or contains every positive real. -/
256theorem selected_amplitudes_eq_zero_or_all_pos
257 (P : sp.X → Prop) (hP : IsInvariantSelector sp P) :
258 (∀ x, P x → sp.A x = 0) ∨ (∀ c : ℝ, 0 < c → ∃ x, P x ∧ sp.A x = c) := by
259 by_cases h : ∃ x, P x ∧ 0 < sp.A x
260 · right
261 obtain ⟨x, hx, hA⟩ := h
262 intro c hc
263 refine ⟨sp.scale ⟨c / sp.A x, div_pos hc hA⟩ x, ?_, ?_⟩
264 · exact (hP _ x).mpr hx
265 · rw [sp.A_homog, div_mul_cancel₀ c (ne_of_gt hA)]
266 · left
267 intro x hx
268 have h1 : sp.A x ≤ 0 := by
269 by_contra hgt
270 push_neg at hgt
271 exact h ⟨x, hx, hgt⟩
272 exact le_antisymm h1 (sp.A_nonneg x)
273
274/-- Consequence: an invariant selector that is satisfied somewhere
275cannot force every selected configuration to have one positive
276amplitude. -/
277theorem no_forced_positive_amplitude
278 (P : sp.X → Prop) (hP : IsInvariantSelector sp P)
279 (a : ℝ) (ha : 0 < a) :
280 (∃ x, P x) → ¬ ∀ x, P x → sp.A x = a := by
281 intro ⟨x0, hx0⟩ hall
282 rcases selected_amplitudes_eq_zero_or_all_pos sp P hP with hz | hallpos
283 · have h0 := hz x0 hx0
284 rw [hall x0 hx0] at h0
285 linarith
286 · obtain ⟨y, hy, hAy⟩ := hallpos (2 * a) (by linarith)
287 have := hall y hy
288 linarith
289
290end ScaledConfigSpace
291
292/-- The positive quadrant as a scaled configuration space, with the
293first coordinate as amplitude. -/
294def quadrantSpace : ScaledConfigSpace where
295 X := { p : ℝ × ℝ // 0 < p.1 ∧ 0 < p.2 }
296 scale := fun c p => ⟨(c.1 * p.1.1, c.1 * p.1.2),
297 mul_pos c.2 p.2.1, mul_pos c.2 p.2.2⟩
298 scale_one := fun p => by ext <;> simp
299 scale_mul := fun c d p => by ext <;> simp [mul_assoc]
300 A := fun p => p.1.1
301 A_nonneg := fun p => le_of_lt p.2.1
302 A_homog := fun c p => rfl
303
304/-- The paper's witness selector: `a = 2b`. -/
305def quadrantSelector : quadrantSpace.X → Prop := fun p => p.1.1 = 2 * p.1.2
306
307theorem quadrantSelector_invariant :
308 quadrantSpace.IsInvariantSelector quadrantSelector := by
309 intro c p
310 show (c.1 * p.1.1 = 2 * (c.1 * p.1.2)) ↔ (p.1.1 = 2 * p.1.2)
311 constructor
312 · intro h
313 have hc : c.1 ≠ 0 := ne_of_gt c.2
314 have h3 : c.1 * (p.1.1 - 2 * p.1.2) = 0 := by rw [mul_sub, h]; ring
315 rcases mul_eq_zero.mp h3 with hc0 | hdiff
316 · exact absurd hc0 hc
317 · linarith
318 · intro h
319 rw [h]; ring
320
321/-- The witness point (2, 1) in the positive quadrant. -/
322def quadrantPoint21 : quadrantSpace.X :=
323 ⟨(2, 1), by norm_num, by norm_num⟩
324
325theorem quadrantPoint21_selected : quadrantSelector quadrantPoint21 := by
326 show (2 : ℝ) = 2 * 1
327 norm_num
328
329theorem quadrantPoint21_amplitude : quadrantSpace.A quadrantPoint21 = 2 := rfl
330
331theorem quadrant_witness :
332 (∃ x, quadrantSelector x ∧ 0 < quadrantSpace.A x) ∧
333 ¬ ∀ x, quadrantSelector x → quadrantSpace.A x = 2 := by
334 refine ⟨⟨quadrantPoint21, quadrantPoint21_selected, ?_⟩, ?_⟩
335 · rw [quadrantPoint21_amplitude]; norm_num
336 · exact quadrantSpace.no_forced_positive_amplitude _
337 quadrantSelector_invariant 2 (by norm_num)
338 ⟨quadrantPoint21, quadrantPoint21_selected⟩
339
340/-- The scale-invariant readout `B(a,b) = a/b`: constant on orbits, and
341pinned to `2` on every selected configuration. This is the content of
342the paper's "what this theorem does not add" remark, kernel-checked. -/
343theorem quadrant_ratio_pinned (p : quadrantSpace.X)
344 (hp : quadrantSelector p) : p.1.1 / p.1.2 = 2 := by
345 have hb : p.1.2 ≠ 0 := ne_of_gt p.2.2
346 have hp' : p.1.1 = 2 * p.1.2 := hp
347 field_simp
348 linarith
349
350theorem quadrant_ratio_scaleInvariant (c : {c : ℝ // 0 < c})
351 (p : quadrantSpace.X) :
352 (quadrantSpace.scale c p).1.1 / (quadrantSpace.scale c p).1.2 =
353 p.1.1 / p.1.2 := by
354 show (c.1 * p.1.1) / (c.1 * p.1.2) = p.1.1 / p.1.2
355 exact mul_div_mul_left _ _ (ne_of_gt c.2)
356
357end AmplitudeForm
358
359end ScaleHomogeneityNoGo
360end Foundation
361end IndisputableMonolith
362