IndisputableMonolith.Foundation.MeasureForcing
IndisputableMonolith/Foundation/MeasureForcing.lean · 820 lines · 62 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Constants
3import IndisputableMonolith.Cost
4import IndisputableMonolith.PhiSupport.Lemmas
5import IndisputableMonolith.Cosmology.DarkEnergyWofZStructural
6import IndisputableMonolith.Cosmology.BITKernelShapeForcing
7
8/-!
9# T9: The Forced Measure on Recognition States
10
11## The problem this module closes
12
13The T-1..T8 chain forces the *shape* of the law: J is the unique cost, φ the
14unique scale, 2³ the minimal period, D = 3 the unique dimension. What the
15chain did not force is the *weighting*: given the allowed recognition
16states, which rule says how much of reality sits in each one? Every
17recurring open instance-selection problem in the library (Born weights,
18chirality selection, δw₀ saturation, η_B prefactor, rung occupancy) is a
19projection of that single missing primitive.
20
21This module derives the rule. **Any admissible weighting of recognition
22states is the geometric φ-measure: weight φ⁻¹ per recognition step,
23equivalently probability ∝ exp(−(ln φ) · cost)** — the Gibbs rule with the
24rate pinned by the self-similar ledger, not chosen.
25
26## The derivation (same machinery that forced J, θ = φ⁻⁴, and K(z))
27
28Lattice layer (recognition is discrete, T2, so this is the fundamental
29layer). A weight rule satisfies exactly two premises:
30
311. **Factorization over independent composition** (`factorizes`). The
32 weight of a composite of independent recognition steps is the product of
33 the weights. This is the multiplicative shadow of ledger cost
34 additivity: a non-factorizing weight would carry correlation with no
35 posting that pays for it.
362. **Per-step self-similar balance** (`step_self_similar`). The single-step
37 weight satisfies ρ = 1/(1+ρ), the reciprocal self-similarity fixed
38 point. By `BITKernelShapeForcing.self_similar_attenuation_forced`
39 this forces ρ = φ⁻¹: the only balance equation available to the ledger
40 is the fixed point of its own forced reciprocal-shift generator; any
41 other ratio imports a second scale, contradicting T6 uniqueness.
42
43These force `w(n) = φ⁻ⁿ` (`RecognitionWeightRule.weight_forced`) — by
44literally the same proof as the BIT kernel rung dilution; the conversion
45`toRungDilution` exhibits the two objects as identical.
46
47Continuum layer. For weight as a function of a real-valued additive cost,
48the premises are factorization over cost addition, antitonicity, and the
49calibrated step `f(1) = φ⁻¹`. The theorem `continuum_weight_forced` proves
50`f(t) = φ⁻ᵗ` for ALL t ≥ 0 — not merely within a power-law class: the
51multiplicative Cauchy equation plus monotonicity pins the function on the
52rationals by roots and on the irrationals by an elementary squeeze. This
53removes the scale-free-class caveat that the kernel module still carried.
54
55Gibbs form. `φ⁻ᵗ = exp(−(ln φ)·t)` (`contWeight_gibbs`): probability
56∝ exp(−cost) with the recognition temperature pinned at 1/ln φ in rung
57units. The *form* is forced by factorization; the *rate* by the
58self-similar step. Nothing is fitted.
59
60## Structure constants of the forced measure (all THEOREM)
61
62* Partition function: `Z = Σ φ⁻ⁿ = φ²` (`partitionZ_eq_phi_sq`). The
63 normalization of the forced measure is φ²; the numerical identity is
64 proved here.
65* Ground-state share: `P(0) = φ⁻²` (`probMass_zero`).
66* Mean occupied rung: `⟨n⟩ = φ` exactly (`meanRung_eq_phi`).
67
68## What the measure does and does not select (honest tags)
69
70* **Chirality (negative result, THEOREM).** The measure is cost-sufficient:
71 equal-cost mirror states get equal weight (`weight_blind_to_label`). So
72 chirality selection CANNOT come from the forced measure at equal J; it
73 requires a J-asymmetry or spontaneous (history) breaking. This sharpens
74 the mass-derivation program by closing one road.
75* **Born rule (OPEN, with a proved regime).** Near the identity tick the
76 forced measure is sub-Gaussian in log-deviation with rate λ/2
77 (`sub_gaussian_in_J`), via J(eᵗ) = cosh t − 1 ≥ t²/2. This is the L²
78 seed; the full Born bridge to recognition Hilbert space is OPEN
79 (closing path: Gaussian regime + the spectral structural identity).
80* **δw₀ (reduced from a free real to one integer, CONDITIONAL).** Under
81 equilibrium occupancy of rungs 0..N, the BIT today-amplitude is
82 `δw₀(N) = J(φ)·(1 − φ^{−(N+1)})` (`deltaW0`); monotone, `< J(φ)`,
83 `→ J(φ)`. For any N it exceeds 0.04 (`deltaW0_gt_004`), and for N ≥ 8 it
84 is within 5% of the ceiling (`deltaW0_near_ceiling`), giving the dated
85 equilibrium prediction `w₀ ∈ (−0.896, −0.88)` (`equilibrium_w0_band`).
86 CONDITIONAL on the equilibrium reading (H-theorem OPEN, below).
87* **H-theorem (OPEN, named).** T9 forces the unique *stationary*
88 weighting. That R̂ evolution converges to it (monotone approach = the RS
89 second law) is the remaining dynamical theorem; until it lands, the
90 aging/cosmology column's monotone-Z premises remain premises.
91
92## Identifications (the existing constants are this measure)
93
94`θ = φ⁻⁴ = w(4)` (`theta_is_lattice_weight`), `ℏ = φ⁻⁵ = w(5)`
95(`hbar_is_lattice_weight`), rung-44 scale `φ⁻⁴⁴ = w(44)`
96(`rung44_is_lattice_weight`), BIT kernel dilution `occ(n) = w(n)`
97(`kernel_dilution_is_measure`); the full repository additionally identifies
98the dimension dilution (`dimension_dilution_is_measure`, outside this
99slice). Previously separate "dilution" and "occupancy" laws are one
100object: the forced measure.
101
102## Status
103
104THEOREM: lattice forcing, continuum forcing (full Cauchy + monotone
105uniqueness), Gibbs form, Z = φ², ⟨n⟩ = φ, sub-Gaussian regime, label
106blindness, δw₀ reduction theorems, all identifications.
107HYPOTHESIS: the per-step balance premise (third instantiation of the
108self-similar-attenuation family: θ, kernel, measure; falsifier: any
109forced-rung sector with per-rung weight ≠ φ⁻¹).
110OPEN: H-theorem (R̂ convergence to the forced measure); Born bridge;
111the cosmic rung count N.
112
113Proposed as **T9** in the forcing chain; wiring into
114`UnifiedForcingChain` is left as an explicit follow-up decision.
115Zero `sorry`, zero new `axiom`.
116-/
117
118namespace IndisputableMonolith
119namespace Foundation
120namespace MeasureForcing
121
122open Constants
123open Cost
124
125noncomputable section
126
127/-! ## §0. The step weight -/
128
129/-- The forced per-step weight `ρ = φ⁻¹`. -/
130def rho : ℝ := 1 / Constants.phi
131
132theorem rho_pos : 0 < rho := by
133 unfold rho
134 exact div_pos one_pos phi_pos
135
136theorem rho_nonneg : 0 ≤ rho := rho_pos.le
137
138theorem rho_lt_one : rho < 1 := by
139 unfold rho
140 rw [div_lt_one phi_pos]
141 exact one_lt_phi
142
143theorem rho_le_one : rho ≤ 1 := rho_lt_one.le
144
145theorem rho_ne_one : rho ≠ 1 := ne_of_lt rho_lt_one
146
147/-- Golden identity for the measure: `1 − ρ = φ⁻²`. The normalization gap
148of the forced measure is the inverse-square of the scale. -/
149theorem one_sub_rho : 1 - rho = 1 / Constants.phi ^ 2 := by
150 unfold rho
151 have hphi : Constants.phi ≠ 0 := phi_ne_zero
152 have hsq : Constants.phi ^ 2 = Constants.phi + 1 := PhiSupport.phi_squared
153 field_simp
154 nlinarith [hsq]
155
156/-- The lattice weight: `w(n) = φ⁻ⁿ` after `n` recognition steps. -/
157def latticeWeight (n : ℕ) : ℝ := (1 / Constants.phi) ^ n
158
159theorem latticeWeight_eq_rho_pow (n : ℕ) : latticeWeight n = rho ^ n := rfl
160
161theorem latticeWeight_pos (n : ℕ) : 0 < latticeWeight n :=
162 pow_pos rho_pos n
163
164/-! ## §1. The lattice layer: the weight rule is forced
165
166Two premises (factorization; per-step self-similar balance), identical in
167form to the rung-dilution premises that force `θ = φ⁻⁴` and the BIT
168kernel. The conversion `toRungDilution` makes the identity literal. -/
169
170/-- A **recognition weight rule**: a positive weight per number of
171recognition steps, factorizing over independent composition, with the
172single-step weight satisfying the reciprocal self-similar balance. -/
173structure RecognitionWeightRule where
174 /-- Weight of a state reached by `n` recognition steps. -/
175 w : ℕ → ℝ
176 /-- Weights are strictly positive. -/
177 w_pos : ∀ n, 0 < w n
178 /-- **Factorization.** Independent composition multiplies weights
179 (multiplicative shadow of ledger cost additivity; unpaid correlation is
180 forbidden). -/
181 factorizes : ∀ m n : ℕ, w (m + n) = w m * w n
182 /-- **Per-step self-similar balance.** The single-step weight is the
183 reciprocal self-similarity fixed point `ρ = 1/(1+ρ)` — the only balance
184 equation expressible with the ledger's forced reciprocal-shift
185 generator. -/
186 step_self_similar : w 1 = 1 / (1 + w 1)
187
188namespace RecognitionWeightRule
189
190/-- A weight rule IS a rung dilution (the kernel object): the premises are
191field-for-field identical. -/
192def toRungDilution (R : RecognitionWeightRule) :
193 Cosmology.BITKernelShapeForcing.RungDilution where
194 occ := R.w
195 occ_pos := R.w_pos
196 composes := R.factorizes
197 one_rung_self_similar := R.step_self_similar
198
199/-- **T9, LATTICE LAYER: the weight rule is forced to `φ⁻ⁿ`.** -/
200theorem weight_forced (R : RecognitionWeightRule) (n : ℕ) :
201 R.w n = latticeWeight n :=
202 (R.toRungDilution).occ_forced n
203
204/-- Any two weight rules agree everywhere: there is exactly one measure. -/
205theorem weight_unique (R S : RecognitionWeightRule) (n : ℕ) :
206 R.w n = S.w n := by
207 rw [R.weight_forced n, S.weight_forced n]
208
209end RecognitionWeightRule
210
211/-! ## §2. Structure constants of the forced measure -/
212
213/-- The partition function `Z = Σ_{n≥0} φ⁻ⁿ`. -/
214def partitionZ : ℝ := ∑' n : ℕ, rho ^ n
215
216/-- **`Z = φ²` exactly.** The normalization of the forced measure is the
217square of the forced scale (numerically the same φ² that gates emergent
218voice density; that identification is a BRIDGE observation, the identity
219here is THEOREM). -/
220theorem partitionZ_eq_phi_sq : partitionZ = Constants.phi ^ 2 := by
221 unfold partitionZ
222 rw [tsum_geometric_of_lt_one rho_nonneg rho_lt_one, one_sub_rho]
223 rw [one_div, inv_inv]
224
225/-- The normalized probability mass at `n` steps: `P(n) = (1−ρ)·ρⁿ`. -/
226def probMass (n : ℕ) : ℝ := (1 - rho) * rho ^ n
227
228theorem probMass_pos (n : ℕ) : 0 < probMass n := by
229 unfold probMass
230 have h1 : 0 < 1 - rho := by linarith [rho_lt_one]
231 exact mul_pos h1 (pow_pos rho_pos n)
232
233/-- The measure is normalized: `Σ P(n) = 1`. -/
234theorem probMass_tsum_one : ∑' n : ℕ, probMass n = 1 := by
235 unfold probMass
236 rw [tsum_mul_left, tsum_geometric_of_lt_one rho_nonneg rho_lt_one]
237 have h1 : 1 - rho ≠ 0 := by
238 have := rho_lt_one; intro h; linarith [sub_eq_zero.mp h]
239 field_simp
240
241/-- The ground-state share is `φ⁻²`. -/
242theorem probMass_zero : probMass 0 = 1 / Constants.phi ^ 2 := by
243 unfold probMass
244 rw [pow_zero, mul_one, one_sub_rho]
245
246/-- The mean occupied rung `⟨n⟩ = Σ n·P(n)`. -/
247def meanRung : ℝ := ∑' n : ℕ, (n : ℝ) * probMass n
248
249/-- **`⟨n⟩ = φ` exactly.** The mean recognition depth of the forced
250measure is the golden ratio itself. -/
251theorem meanRung_eq_phi : meanRung = Constants.phi := by
252 unfold meanRung
253 have hre : (fun n : ℕ => (n : ℝ) * probMass n)
254 = fun n : ℕ => (1 - rho) * ((n : ℝ) * rho ^ n) := by
255 funext n; unfold probMass; ring
256 rw [hre, tsum_mul_left]
257 have hnorm : ‖rho‖ < 1 := by
258 rw [Real.norm_eq_abs, abs_of_pos rho_pos]; exact rho_lt_one
259 rw [tsum_coe_mul_geometric_of_norm_lt_one hnorm]
260 -- (1 − ρ) · ρ/(1−ρ)² = ρ/(1−ρ) = φ⁻¹·φ² = φ
261 rw [one_sub_rho]
262 unfold rho
263 have hphi : Constants.phi ≠ 0 := phi_ne_zero
264 field_simp
265
266/-! ## §3. The continuum layer: full Cauchy + monotone uniqueness
267
268Weight as a function of a real additive cost. Factorization +
269antitonicity + the calibrated step force `f(t) = ρᵗ` for ALL `t ≥ 0`,
270with no power-law-class restriction: rationals by roots, irrationals by
271an elementary order squeeze. -/
272
273section Continuum
274
275variable {f : ℝ → ℝ}
276
277/-- Factorization over cost addition on the nonneg domain. -/
278def Factorizes (f : ℝ → ℝ) : Prop :=
279 ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → f (a + b) = f a * f b
280
281theorem f_zero (hadd : Factorizes f)
282 (hanti : AntitoneOn f (Set.Ici 0)) (hstep : f 1 = rho) :
283 f 0 = 1 := by
284 have h00 : f 0 = f 0 * f 0 := by
285 have := hadd 0 0 le_rfl le_rfl
286 simpa using this
287 have hge : rho ≤ f 0 := by
288 have h := hanti (Set.mem_Ici.mpr le_rfl) (Set.mem_Ici.mpr zero_le_one)
289 zero_le_one
290 rwa [hstep] at h
291 have hpos : 0 < f 0 := lt_of_lt_of_le rho_pos hge
292 have hfac : f 0 * (f 0 - 1) = 0 := by nlinarith [h00]
293 rcases mul_eq_zero.mp hfac with h | h
294 · exact absurd h (ne_of_gt hpos)
295 · linarith [sub_eq_zero.mp h]
296
297theorem f_nmul (hadd : Factorizes f)
298 (hanti : AntitoneOn f (Set.Ici 0)) (hstep : f 1 = rho)
299 (x : ℝ) (hx : 0 ≤ x) :
300 ∀ k : ℕ, f ((k : ℝ) * x) = f x ^ k := by
301 intro k
302 induction k with
303 | zero => simpa using f_zero hadd hanti hstep
304 | succ k ih =>
305 have harg : ((k + 1 : ℕ) : ℝ) * x = (k : ℝ) * x + x := by
306 push_cast; ring
307 have hkx : 0 ≤ (k : ℝ) * x := by positivity
308 rw [harg, hadd _ _ hkx hx, ih, pow_succ]
309
310theorem f_nonneg_of_nonneg (hadd : Factorizes f)
311 (x : ℝ) (hx : 0 ≤ x) : 0 ≤ f x := by
312 have hh := hadd (x / 2) (x / 2) (by positivity) (by positivity)
313 have harg : x / 2 + x / 2 = x := by ring
314 rw [harg] at hh
315 rw [hh]
316 exact mul_self_nonneg _
317
318/-- The rational case: `f(p/q) = ρ^(p/q)` by uniqueness of positive
319`q`-th roots. -/
320theorem f_rat (hadd : Factorizes f)
321 (hanti : AntitoneOn f (Set.Ici 0)) (hstep : f 1 = rho)
322 (p q : ℕ) (hq : q ≠ 0) :
323 f ((p : ℝ) / (q : ℝ)) = rho ^ ((p : ℝ) / (q : ℝ)) := by
324 have hqR : ((q : ℕ) : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hq
325 set x : ℝ := (p : ℝ) / (q : ℝ) with hxdef
326 have hx0 : 0 ≤ x := by positivity
327 -- f(x)^q = ρ^p
328 have h1 : f ((q : ℝ) * x) = f x ^ q := f_nmul hadd hanti hstep x hx0 q
329 have harg : (q : ℝ) * x = (p : ℝ) := by
330 rw [hxdef]; field_simp
331 have h2 : f ((p : ℝ)) = rho ^ p := by
332 have := f_nmul hadd hanti hstep 1 zero_le_one p
333 simpa [hstep] using this
334 have hkey : f x ^ q = rho ^ p := by rw [← h1, harg, h2]
335 -- (ρ^x)^q = ρ^p
336 have hpow : (rho ^ x) ^ q = rho ^ p := by
337 rw [← Real.rpow_natCast (rho ^ x) q, ← Real.rpow_mul rho_nonneg]
338 have hmul : x * (q : ℝ) = (p : ℝ) := by rw [hxdef]; field_simp
339 rw [hmul, Real.rpow_natCast]
340 -- nonneg q-th roots agree
341 have hfx : 0 ≤ f x := f_nonneg_of_nonneg hadd x hx0
342 have hrx : 0 ≤ rho ^ x := Real.rpow_nonneg rho_nonneg x
343 exact (pow_left_inj₀ hfx hrx hq).mp (hkey.trans hpow.symm)
344
345/-- The rational case via the `ℚ`-cast. -/
346theorem f_ratCast (hadd : Factorizes f)
347 (hanti : AntitoneOn f (Set.Ici 0)) (hstep : f 1 = rho)
348 (q : ℚ) (hq0 : 0 ≤ (q : ℝ)) :
349 f ((q : ℝ)) = rho ^ ((q : ℝ)) := by
350 have hq0' : 0 ≤ q := by exact_mod_cast hq0
351 have hnum : 0 ≤ q.num := Rat.num_nonneg.mpr hq0'
352 have hden : q.den ≠ 0 := q.den_nz
353 have hp : ((q.num.toNat : ℕ) : ℝ) = ((q.num : ℤ) : ℝ) := by
354 exact_mod_cast Int.toNat_of_nonneg hnum
355 have hcast : ((q : ℝ)) = ((q.num.toNat : ℕ) : ℝ) / ((q.den : ℕ) : ℝ) := by
356 rw [Rat.cast_def, hp]
357 rw [hcast]
358 exact f_rat hadd hanti hstep q.num.toNat q.den hden
359
360/-- **T9, CONTINUUM LAYER (full uniqueness).** Any factorizing, antitone
361weight with the calibrated step `f(1) = φ⁻¹` equals `φ⁻ᵗ` at every
362`t ≥ 0`. No power-law-class restriction: this is the multiplicative
363Cauchy equation pinned by monotonicity. -/
364theorem continuum_weight_forced (hadd : Factorizes f)
365 (hanti : AntitoneOn f (Set.Ici 0)) (hstep : f 1 = rho) :
366 ∀ t : ℝ, 0 ≤ t → f t = rho ^ t := by
367 intro t ht
368 rcases eq_or_lt_of_le ht with h0 | hpos
369 · rw [← h0, Real.rpow_zero]
370 exact f_zero hadd hanti hstep
371 -- t > 0. Set L := f t and squeeze with rationals.
372 set L : ℝ := f t with hL
373 -- upper rationals: t ≤ q ⇒ ρ^q ≤ L
374 have hub : ∀ q : ℚ, t ≤ (q : ℝ) → rho ^ ((q : ℝ)) ≤ L := by
375 intro q hq
376 have hq0 : (0 : ℝ) ≤ (q : ℝ) := le_trans hpos.le hq
377 have := hanti (Set.mem_Ici.mpr hpos.le) (Set.mem_Ici.mpr hq0) hq
378 rwa [f_ratCast hadd hanti hstep q hq0] at this
379 -- lower rationals: 0 ≤ q ≤ t ⇒ L ≤ ρ^q
380 have hlb : ∀ q : ℚ, 0 ≤ (q : ℝ) → (q : ℝ) ≤ t → L ≤ rho ^ ((q : ℝ)) := by
381 intro q hq0 hq
382 have := hanti (Set.mem_Ici.mpr hq0) (Set.mem_Ici.mpr hpos.le) hq
383 rwa [f_ratCast hadd hanti hstep q hq0] at this
384 -- L > 0
385 have hLpos : 0 < L := by
386 obtain ⟨q, hq⟩ := exists_rat_gt t
387 exact lt_of_lt_of_le (Real.rpow_pos_of_pos rho_pos _) (hub q hq.le)
388 have hrt_pos : 0 < rho ^ t := Real.rpow_pos_of_pos rho_pos t
389 have hlogrho_neg : Real.log rho < 0 := Real.log_neg rho_pos rho_lt_one
390 -- trichotomy
391 rcases lt_trichotomy L (rho ^ t) with hlt | heq | hgt
392 · -- L < ρ^t: find rational q > t with ρ^q > L. Contradiction with hub.
393 exfalso
394 have hlog : Real.log L < t * Real.log rho := by
395 have := Real.log_lt_log hLpos hlt
396 rwa [Real.log_rpow rho_pos] at this
397 have hkey : t < Real.log L / Real.log rho := by
398 rw [lt_div_iff_of_neg hlogrho_neg]
399 linarith [hlog]
400 obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn hkey
401 have hcontra : L < rho ^ ((q : ℝ)) := by
402 have hq2' : Real.log L < (q : ℝ) * Real.log rho := by
403 have := (lt_div_iff_of_neg hlogrho_neg).mp hq2
404 linarith
405 have : Real.exp (Real.log L) < Real.exp (Real.log rho * (q : ℝ)) := by
406 rw [Real.exp_lt_exp]; linarith
407 rwa [Real.exp_log hLpos, ← Real.rpow_def_of_pos rho_pos] at this
408 exact absurd (hub q hq1.le) (not_le.mpr hcontra)
409 · exact heq
410 · -- L > ρ^t: find rational 0 ≤ q < t with ρ^q < L. Contradiction with hlb.
411 exfalso
412 have hlog : t * Real.log rho < Real.log L := by
413 have := Real.log_lt_log hrt_pos hgt
414 rwa [Real.log_rpow rho_pos] at this
415 have hkey : Real.log L / Real.log rho < t := by
416 rw [div_lt_iff_of_neg hlogrho_neg]
417 linarith [hlog]
418 have hmax : max (Real.log L / Real.log rho) 0 < t := max_lt hkey hpos
419 obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn hmax
420 have hq0 : (0 : ℝ) ≤ (q : ℝ) :=
421 le_of_lt (lt_of_le_of_lt (le_max_right _ _) hq1)
422 have hcontra : rho ^ ((q : ℝ)) < L := by
423 have hqgt : Real.log L / Real.log rho < (q : ℝ) :=
424 lt_of_le_of_lt (le_max_left _ _) hq1
425 have hq2' : (q : ℝ) * Real.log rho < Real.log L := by
426 have := (div_lt_iff_of_neg hlogrho_neg).mp hqgt
427 linarith
428 have : Real.exp (Real.log rho * (q : ℝ)) < Real.exp (Real.log L) := by
429 rw [Real.exp_lt_exp]; linarith
430 rwa [Real.exp_log hLpos, ← Real.rpow_def_of_pos rho_pos] at this
431 exact absurd (hlb q hq0 hq2.le) (not_le.mpr hcontra)
432
433end Continuum
434
435/-! ## §4. The Gibbs form: probability ∝ exp(−cost·ln φ) -/
436
437/-- The forced continuum weight `w(t) = ρᵗ = φ⁻ᵗ`. -/
438def contWeight (t : ℝ) : ℝ := rho ^ t
439
440/-- The forced weight in inverse-φ-power form. -/
441theorem contWeight_eq_phi_rpow_neg (t : ℝ) :
442 contWeight t = Constants.phi ^ (-t) := by
443 unfold contWeight rho
444 rw [one_div, Real.inv_rpow phi_pos.le, ← Real.rpow_neg phi_pos.le]
445
446/-- **THE GIBBS FORM.** The forced weight is the exponential of (−) the
447cost, with the rate pinned at `ln φ` per recognition step:
448`w(t) = exp(−(ln φ)·t)`. Probability ∝ exp(−cost), nothing fitted. -/
449theorem contWeight_gibbs (t : ℝ) :
450 contWeight t = Real.exp (-(Real.log Constants.phi) * t) := by
451 unfold contWeight
452 rw [Real.rpow_def_of_pos rho_pos]
453 congr 1
454 unfold rho
455 rw [one_div, Real.log_inv]
456
457/-- The forced weight satisfies all three continuum premises
458(non-vacuity of the uniqueness theorem). -/
459theorem contWeight_satisfies_premises :
460 Factorizes contWeight ∧
461 AntitoneOn contWeight (Set.Ici 0) ∧
462 contWeight 1 = rho :=
463 ⟨fun a b _ _ => Real.rpow_add rho_pos a b,
464 fun _ _ _ _ hab => Real.rpow_le_rpow_of_exponent_ge rho_pos rho_le_one hab,
465 Real.rpow_one rho⟩
466
467/-! ## §5. The Born regime: the forced measure is sub-Gaussian in
468log-deviation
469
470`J(eᵗ) = cosh t − 1 ≥ t²/2`, so `exp(−λ·J)` is dominated by the Gaussian
471`exp(−λt²/2)`. This is the L² seed of the Born bridge (the full bridge is
472OPEN). -/
473
474/-- The J-cost of a state at log-deviation `t`: `J(eᵗ) = cosh t − 1`. -/
475theorem Jcost_exp_eq_cosh_sub_one (t : ℝ) :
476 Cost.Jcost (Real.exp t) = Real.cosh t - 1 := by
477 unfold Cost.Jcost
478 rw [Real.cosh_eq, ← Real.exp_neg]
479
480private lemma half_sq_le_cosh_sub_one_of_nonneg (s : ℝ) (hs : 0 ≤ s) :
481 s ^ 2 / 2 ≤ Real.cosh s - 1 := by
482 have hu : 0 ≤ s / 2 := by linarith
483 have hsinh : s / 2 ≤ Real.sinh (s / 2) := Real.self_le_sinh_iff.mpr hu
484 have hkey : Real.cosh s = 2 * Real.sinh (s / 2) ^ 2 + 1 := by
485 have h2 : 2 * (s / 2) = s := by ring
486 calc Real.cosh s = Real.cosh (2 * (s / 2)) := by rw [h2]
487 _ = Real.cosh (s / 2) ^ 2 + Real.sinh (s / 2) ^ 2 :=
488 Real.cosh_two_mul (s / 2)
489 _ = (Real.sinh (s / 2) ^ 2 + 1) + Real.sinh (s / 2) ^ 2 := by
490 rw [Real.cosh_sq]
491 _ = 2 * Real.sinh (s / 2) ^ 2 + 1 := by ring
492 nlinarith [hsinh, hu]
493
494/-- `cosh t − 1 ≥ t²/2` for all real `t`. -/
495theorem half_sq_le_cosh_sub_one (t : ℝ) :
496 t ^ 2 / 2 ≤ Real.cosh t - 1 := by
497 rcases le_or_gt 0 t with h | h
498 · exact half_sq_le_cosh_sub_one_of_nonneg t h
499 · have h' := half_sq_le_cosh_sub_one_of_nonneg (-t) (by linarith)
500 rw [Real.cosh_neg] at h'
501 calc t ^ 2 / 2 = (-t) ^ 2 / 2 := by ring
502 _ ≤ Real.cosh t - 1 := h'
503
504/-- **SUB-GAUSSIAN REGIME (the L² seed).** The forced measure at rate
505`λ ≥ 0` in the J-coordinate is dominated by the Gaussian of variance
506`1/λ` in log-deviation: `exp(−λ·J(eᵗ)) ≤ exp(−λt²/2)`. -/
507theorem sub_gaussian_in_J (lam t : ℝ) (hlam : 0 ≤ lam) :
508 Real.exp (-lam * Cost.Jcost (Real.exp t)) ≤
509 Real.exp (-lam * (t ^ 2 / 2)) := by
510 rw [Jcost_exp_eq_cosh_sub_one]
511 rw [Real.exp_le_exp]
512 have h := half_sq_le_cosh_sub_one t
513 nlinarith [mul_le_mul_of_nonneg_left h hlam]
514
515/-! ## §6. Identifications: the existing constants ARE this measure -/
516
517/-- `θ = φ⁻⁴` is the forced measure at 4 steps. (Public slice: stated
518against the defining display `1/φ⁴`; the full repository binds this value
519to `Cosmology.DarkEnergyThetaPhiFour.thetaPhiFour`, which is definitionally
520identical.) -/
521theorem theta_is_lattice_weight :
522 (1 : ℝ) / Constants.phi ^ 4 = latticeWeight 4 := by
523 unfold latticeWeight
524 rw [div_pow, one_pow]
525
526/-- `ℏ = φ⁻⁵` is the forced measure at 5 steps. -/
527theorem hbar_is_lattice_weight :
528 Constants.hbar = latticeWeight 5 := by
529 rw [Constants.hbar_eq_phi_inv_fifth]
530 unfold latticeWeight
531 rw [Real.rpow_neg phi_pos.le,
532 show ((5 : ℝ)) = ((5 : ℕ) : ℝ) by norm_num, Real.rpow_natCast,
533 div_pow, one_pow, one_div]
534
535/-- The rung-44 scale `φ⁻⁴⁴` is the forced measure at 44 steps. -/
536theorem rung44_is_lattice_weight :
537 Cosmology.DarkEnergyWofZStructural.phi_neg_44 = latticeWeight 44 := by
538 unfold Cosmology.DarkEnergyWofZStructural.phi_neg_44 latticeWeight
539 rw [zpow_neg, show ((44 : ℤ)) = ((44 : ℕ) : ℤ) by norm_num,
540 zpow_natCast, div_pow, one_pow, one_div]
541
542/-- The BIT kernel rung dilution IS the forced measure. -/
543theorem kernel_dilution_is_measure
544 (L : Cosmology.BITKernelShapeForcing.RungDilution) (n : ℕ) :
545 L.occ n = latticeWeight n :=
546 L.occ_forced n
547
548/- NOTE (public slice): the full repository additionally proves
549`dimension_dilution_is_measure` (the `θ = φ⁻⁴` dimension-uniform dilution IS
550the forced measure) against `Cosmology.DarkEnergyPhiDilutionDerivation`,
551which is outside this slice. The lattice-layer instance retained above
552(`kernel_dilution_is_measure`) carries the same forcing content via the
553self-contained `BITKernelShapeForcing.RungDilution.occ_forced`. -/
554
555/-! ## §7. Cost blindness: the measure cannot select chirality
556
557The forced measure is a function of cost alone. Mirror configurations with
558equal J receive equal weight, so chirality selection requires a J-asymmetry
559or spontaneous (history) breaking — it CANNOT come from T9. This is a
560proved negative result that closes one road for the mass-derivation program. -/
561
562/-- A labeled recognition state: a cost plus a binary label (e.g. L/R
563chirality). -/
564structure LabeledState where
565 cost : ℝ
566 label : Bool
567
568/-- A cost-sufficient weight on labeled states: the weight factors through
569the cost (T9's cost-sufficiency premise). -/
570structure CostSufficientWeight where
571 w : LabeledState → ℝ
572 cost_sufficient : ∀ s t : LabeledState, s.cost = t.cost → w s = w t
573
574/-- **CHIRALITY NO-GO.** Any cost-sufficient weight assigns equal weight
575to the two mirror labels at every cost. -/
576theorem weight_blind_to_label (W : CostSufficientWeight) (c : ℝ) :
577 W.w ⟨c, true⟩ = W.w ⟨c, false⟩ :=
578 W.cost_sufficient _ _ rfl
579
580/-! ## §8. The δw₀ reduction: from a free real to one integer
581
582Under equilibrium occupancy of cosmic-Z rungs `0..N`, the BIT
583today-amplitude is the measure-weighted saturation times the
584phantom-Carnot ceiling. -/
585
586/-- Closed form of `J(φ)` (public; the private copies elsewhere are not
587importable). -/
588theorem Jcost_phi_closed_form : Cost.Jcost Constants.phi = Constants.phi - 3 / 2 := by
589 unfold Cost.Jcost
590 have hphi : Constants.phi ≠ 0 := phi_ne_zero
591 have hsq : Constants.phi ^ 2 = Constants.phi + 1 := PhiSupport.phi_squared
592 field_simp
593 nlinarith [sq_pos_of_pos phi_pos, hsq]
594
595theorem Jcost_phi_gt_011 : 0.11 < Cost.Jcost Constants.phi := by
596 rw [Jcost_phi_closed_form]
597 linarith [phi_gt_onePointSixOne]
598
599/-- The cumulative measure of rungs `0..N` (the Z-saturation fraction). -/
600def saturation (N : ℕ) : ℝ := ∑ n ∈ Finset.range (N + 1), probMass n
601
602/-- Closed form: `saturation N = 1 − ρ^(N+1)`. -/
603theorem saturation_closed (N : ℕ) : saturation N = 1 - rho ^ (N + 1) := by
604 unfold saturation probMass
605 rw [← Finset.mul_sum, geom_sum_eq rho_ne_one]
606 have h1 : rho - 1 ≠ 0 := by
607 intro h; exact rho_ne_one (by linarith [sub_eq_zero.mp h])
608 field_simp
609 ring
610
611theorem saturation_lt_one (N : ℕ) : saturation N < 1 := by
612 rw [saturation_closed]
613 have : 0 < rho ^ (N + 1) := pow_pos rho_pos _
614 linarith
615
616theorem saturation_monotone : Monotone saturation := by
617 intro N M h
618 rw [saturation_closed, saturation_closed]
619 have hp : rho ^ (M + 1) ≤ rho ^ (N + 1) :=
620 pow_le_pow_of_le_one rho_nonneg rho_le_one (by omega)
621 linarith
622
623/-- The saturation tends to 1: deep occupancy exhausts the measure. -/
624theorem saturation_tendsto_one :
625 Filter.Tendsto saturation Filter.atTop (nhds 1) := by
626 have hfun : saturation = fun N => 1 - rho ^ (N + 1) :=
627 funext saturation_closed
628 rw [hfun]
629 have hpow : Filter.Tendsto (fun N : ℕ => rho ^ (N + 1))
630 Filter.atTop (nhds 0) := by
631 have hbase := tendsto_pow_atTop_nhds_zero_of_lt_one rho_nonneg rho_lt_one
632 exact hbase.comp (Filter.tendsto_add_atTop_nat 1)
633 have hsub : Filter.Tendsto (fun N : ℕ => 1 - rho ^ (N + 1))
634 Filter.atTop (nhds (1 - 0)) :=
635 Filter.Tendsto.sub tendsto_const_nhds hpow
636 simpa using hsub
637
638/-- The equilibrium BIT today-amplitude with occupancy depth `N`:
639`δw₀(N) = J(φ)·saturation(N)`. The free real `δw₀` is reduced to one
640integer. -/
641def deltaW0 (N : ℕ) : ℝ := Cost.Jcost Constants.phi * saturation N
642
643/-- `δw₀(N)` never reaches the ceiling. -/
644theorem deltaW0_lt_ceiling (N : ℕ) :
645 deltaW0 N < Cost.Jcost Constants.phi := by
646 unfold deltaW0
647 have hJ : 0 < Cost.Jcost Constants.phi := Constants.Jcost_phi_pos
648 nlinarith [saturation_lt_one N]
649
650/-- `δw₀(N) → J(φ)`: the ceiling is the deep-occupancy limit. -/
651theorem deltaW0_tendsto_ceiling :
652 Filter.Tendsto deltaW0 Filter.atTop (nhds (Cost.Jcost Constants.phi)) := by
653 unfold deltaW0
654 have := Filter.Tendsto.const_mul (Cost.Jcost Constants.phi) saturation_tendsto_one
655 simpa using this
656
657/-- Numerical step bound: `ρ < 0.6212`. -/
658theorem rho_lt_06212 : rho < 0.6212 := by
659 unfold rho
660 rw [div_lt_iff₀ phi_pos]
661 nlinarith [phi_gt_onePointSixOne]
662
663/-- **Equilibrium excludes exact ΛCDM.** For ANY occupancy depth `N`,
664`δw₀(N) > 0.04`: under the equilibrium reading the deviation cannot
665vanish. A confirmed `|w₀ + 1| < 0.04` falsifies equilibrium T9 occupancy
666(not T9 itself). -/
667theorem deltaW0_gt_004 (N : ℕ) : 0.04 < deltaW0 N := by
668 have hmono := saturation_monotone (Nat.zero_le N)
669 have hsat0 : 0.37 < saturation 0 := by
670 rw [saturation_closed]
671 have : rho ^ (0 + 1) = rho := by ring
672 rw [this]
673 linarith [rho_lt_06212]
674 have hJ := Jcost_phi_gt_011
675 have hsat : 0.37 < saturation N := lt_of_lt_of_le hsat0 hmono
676 unfold deltaW0
677 nlinarith [hJ, hsat]
678
679/-- Numerical: `ρ⁹ < 0.014` (so nine rungs of occupancy already exhaust
68098.6% of the measure). -/
681theorem rho_pow_nine_lt : rho ^ 9 < 0.014 := by
682 have h1 : rho ^ 9 < 0.6212 ^ 9 :=
683 pow_lt_pow_left₀ rho_lt_06212 rho_nonneg (by norm_num)
684 have h2 : (0.6212 : ℝ) ^ 9 < 0.014 := by norm_num
685 linarith
686
687/-- **Near-ceiling saturation.** For `N ≥ 8`, `δw₀(N) > 0.95·J(φ)`:
688equilibrium occupancy deeper than eight rungs pins the amplitude within
6895% of the phantom-Carnot ceiling. -/
690theorem deltaW0_near_ceiling (N : ℕ) (hN : 8 ≤ N) :
691 0.95 * Cost.Jcost Constants.phi < deltaW0 N := by
692 have hsat8 : 0.98 < saturation 8 := by
693 rw [saturation_closed]
694 have h9 : rho ^ (8 + 1) = rho ^ 9 := by norm_num
695 rw [h9]
696 linarith [rho_pow_nine_lt]
697 have hmono := saturation_monotone hN
698 have hsat : 0.98 < saturation N := lt_of_lt_of_le hsat8 hmono
699 have hJ : 0 < Cost.Jcost Constants.phi := Constants.Jcost_phi_pos
700 unfold deltaW0
701 nlinarith [hJ, hsat]
702
703/-- **THE DATED EQUILIBRIUM BAND (2026-06-09).** For occupancy `N ≥ 8`,
704the equilibrium prediction is `w₀ = −1 + δw₀(N) ∈ (−0.896, −0.88)`.
705CONDITIONAL on the equilibrium reading (H-theorem OPEN); jointly
706falsified with it by DESI Y3+/Roman/Euclid outside the band. -/
707theorem equilibrium_w0_band (N : ℕ) (hN : 8 ≤ N) :
708 -0.896 < -1 + deltaW0 N ∧ -1 + deltaW0 N < -0.88 := by
709 have hnear := deltaW0_near_ceiling N hN
710 have hceil := deltaW0_lt_ceiling N
711 have hJlo := Jcost_phi_gt_011
712 have hJhi : Cost.Jcost Constants.phi < 0.12 :=
713 Cosmology.BITKernelShapeForcing.jcost_phi_lt_012
714 constructor
715 · nlinarith
716 · nlinarith
717
718/-! ## §9. Master certificate and the T9 one-statement -/
719
720/-- **T9 MASTER CERTIFICATE: THE FORCED MEASURE (dated 2026-06-09).**
721
7221. Lattice forcing: every weight rule is `φ⁻ⁿ`.
7232. Uniqueness: any two weight rules agree.
7243. Continuum forcing: every factorizing antitone calibrated weight is
725 `φ⁻ᵗ` (full Cauchy + monotone uniqueness, no class restriction).
7264. Non-vacuity: the forced weight satisfies the premises.
7275. Gibbs form: `w(t) = exp(−(ln φ)·t)`.
7286. Partition function `Z = φ²`; ground share `φ⁻²`; mean rung `φ`.
7297. Sub-Gaussian Born regime.
7308. Cost blindness (chirality no-go).
7319. The constants `θ = φ⁻⁴`, `ℏ = φ⁻⁵`, rung-44, and the kernel dilution
732 are all instances of the one measure (the full repository adds the
733 dimension dilution).
73410. δw₀ reduction: bounded, monotone, `→ J(φ)`, `> 0.04` always, near
735 ceiling for `N ≥ 8`. -/
736structure MeasureForcingCert where
737 lattice_forced :
738 ∀ (R : RecognitionWeightRule) (n : ℕ), R.w n = latticeWeight n
739 lattice_unique :
740 ∀ (R S : RecognitionWeightRule) (n : ℕ), R.w n = S.w n
741 continuum_forced :
742 ∀ f : ℝ → ℝ, Factorizes f → AntitoneOn f (Set.Ici 0) → f 1 = rho →
743 ∀ t : ℝ, 0 ≤ t → f t = rho ^ t
744 nonvacuous :
745 Factorizes contWeight ∧ AntitoneOn contWeight (Set.Ici 0) ∧
746 contWeight 1 = rho
747 gibbs_form :
748 ∀ t : ℝ, contWeight t = Real.exp (-(Real.log Constants.phi) * t)
749 partition_eq : partitionZ = Constants.phi ^ 2
750 ground_share : probMass 0 = 1 / Constants.phi ^ 2
751 mean_rung : meanRung = Constants.phi
752 sub_gaussian :
753 ∀ lam t : ℝ, 0 ≤ lam →
754 Real.exp (-lam * Cost.Jcost (Real.exp t)) ≤
755 Real.exp (-lam * (t ^ 2 / 2))
756 chirality_no_go :
757 ∀ (W : CostSufficientWeight) (c : ℝ),
758 W.w ⟨c, true⟩ = W.w ⟨c, false⟩
759 theta_instance :
760 (1 : ℝ) / Constants.phi ^ 4 = latticeWeight 4
761 hbar_instance : Constants.hbar = latticeWeight 5
762 rung44_instance :
763 Cosmology.DarkEnergyWofZStructural.phi_neg_44 = latticeWeight 44
764 kernel_instance :
765 ∀ (L : Cosmology.BITKernelShapeForcing.RungDilution) (n : ℕ),
766 L.occ n = latticeWeight n
767 delta_w0_window :
768 ∀ N : ℕ, 0.04 < deltaW0 N ∧ deltaW0 N < Cost.Jcost Constants.phi
769 delta_w0_equilibrium_band :
770 ∀ N : ℕ, 8 ≤ N →
771 -0.896 < -1 + deltaW0 N ∧ -1 + deltaW0 N < -0.88
772
773/-- The master certificate is inhabited. -/
774def measureForcingCert : MeasureForcingCert where
775 lattice_forced := fun R n => R.weight_forced n
776 lattice_unique := fun R S n => R.weight_unique S n
777 continuum_forced := fun _ hadd hanti hstep => continuum_weight_forced hadd hanti hstep
778 nonvacuous := contWeight_satisfies_premises
779 gibbs_form := contWeight_gibbs
780 partition_eq := partitionZ_eq_phi_sq
781 ground_share := probMass_zero
782 mean_rung := meanRung_eq_phi
783 sub_gaussian := sub_gaussian_in_J
784 chirality_no_go := weight_blind_to_label
785 theta_instance := theta_is_lattice_weight
786 hbar_instance := hbar_is_lattice_weight
787 rung44_instance := rung44_is_lattice_weight
788 kernel_instance := kernel_dilution_is_measure
789 delta_w0_window := fun N => ⟨deltaW0_gt_004 N, deltaW0_lt_ceiling N⟩
790 delta_w0_equilibrium_band := fun N hN => equilibrium_w0_band N hN
791
792/-- **T9, ONE STATEMENT.** Reality weights allowed recognition states by
793one unique rule: weight `φ⁻¹` per recognition step on the lattice,
794`exp(−(ln φ)·cost)` in the continuum; with partition function `φ²` and
795mean rung `φ`; cost-blind (no chirality selection); and reducing the BIT
796amplitude to one integer with equilibrium band
797`w₀ ∈ (−0.896, −0.88)` for `N ≥ 8`. -/
798theorem t9_measure_forced :
799 (∀ (R : RecognitionWeightRule) (n : ℕ), R.w n = latticeWeight n) ∧
800 (∀ f : ℝ → ℝ, Factorizes f → AntitoneOn f (Set.Ici 0) → f 1 = rho →
801 ∀ t : ℝ, 0 ≤ t → f t = rho ^ t) ∧
802 partitionZ = Constants.phi ^ 2 ∧
803 meanRung = Constants.phi ∧
804 (∀ (W : CostSufficientWeight) (c : ℝ),
805 W.w ⟨c, true⟩ = W.w ⟨c, false⟩) ∧
806 (∀ N : ℕ, 8 ≤ N →
807 -0.896 < -1 + deltaW0 N ∧ -1 + deltaW0 N < -0.88) :=
808 ⟨fun R n => R.weight_forced n,
809 fun _ hadd hanti hstep => continuum_weight_forced hadd hanti hstep,
810 partitionZ_eq_phi_sq,
811 meanRung_eq_phi,
812 weight_blind_to_label,
813 equilibrium_w0_band⟩
814
815end
816
817end MeasureForcing
818end Foundation
819end IndisputableMonolith
820