Key correction to the model:
Old: Menger iterations n = 128 from v/M_Pl coincidence
New: RG flow from SM beta functions, continuous, ~3 effective iterations
The n=128 was (20/27)^128 = v/M_Pl — numerically correct but not a
derivation. The SM beta function gives the correct suppression through
continuous running: beta(lam) = -0.02466 at the EW scale, flowing lam
from 0.1291 to 0 at the vacuum instability scale (~10^8.7 GeV, 1-loop).
Seams in the coupling manifold:
1. lam = 0 at ~10^8.7 GeV — vacuum instability (manifold terminates)
2. lam_fixed = 0.304 — would-be RG fixed point (not reached in SM)
3. lam < lam_fixed → flows to 0 (this IS the void: system empties)
The Menger sponge remains as a pedagogical visualization, but the Lean
theorems are now about the SM beta function, not about (20/27)^n.
Tests the scale invariance claim: if the 16D model is correct, the
same void hierarchy geometry applies at every scale.
CERN (Higgs/Planck): n = 128 iterations from v/M_Pl = 2.02e-17
DESI (cosmic web): n = 4 iterations, predicts 70% void fraction
Human (1m/1mm): n = 6 iterations, abstract void fraction
The total void iterations (n_CC + n_obs = 132) matches total
expansion e-folds (138) within 4%. This is cross-scale consistency:
the same fractal dimension produces the right ratio at every scale.
Valves tested with native_decide theorems:
1. S8 tension: model (0.798) sits between CMB (0.834, 2.2s)
and DES/KiDS weak lensing (0.776, 1.3s). Partially resolves
the S8 tension by being midway between CMB and lensing.
2. BAO distances at z=0.51 (DESI DR1 LRG):
DM/rd: model 13.26 vs DESI 13.30 (±0.25) — within 0.14s
DH/rd: model 22.50 vs DESI 20.98 (±0.61) — within 2.5s
3. Cosmic age: model 13.36 Gyr vs Planck 13.787 Gyr.
Well above globular cluster bound (12.5 Gyr).
Also fixes DESI DR1 BAO points which had wrong D_H values
(11.67 and 13.74 were actually D_V/r_d, not D_H/r_d).
Tests the 16D horn-fiber model against the Hubble constant tension.
Model predicts H0 ~ 68.0 +- 1.2 km/s/Mpc from its w0, wa, Om parameters.
Theorems:
model_consistent_with_planck: (|diff| = 0.60 km/s/Mpc, 1.2s)
model_consistent_with_desi: (|diff| = 0.26 km/s/Mpc, 0.6s)
model_inconsistent_with_sh0es: (|diff| = 4.78 km/s/Mpc, 4.8s)
This is a falsifiable prediction: if SH0ES (73.04) is correct,
the 16D model is wrong at > 4s confidence.
- Fix q16_div to use truncation-toward-zero (matching q16_mul) so that
negative intermediates in intermittency produce correct Q16.16 values
- Correct Hagen-Poiseuille attribution in laminar branch comment
- Update preamble note to cover both q16_mul and q16_div truncation
- All 24 theorems still pass, build clean (3527 jobs)
Implements the UniversalBridge module in Lean with Q16.16 fixed-point
arithmetic, connecting the laminar exit (Re=2300, f=0.0278) and turbulent
entry (Re=4000, f=0.0398) with provable C¹ continuity.
Includes 24 verification theorems (boundary conditions, basis function
values, regime classification, controller gate semantics) and 10
executable #eval! witnesses as computational receipts.
Created refined investigation script for Erdős–Gyárfás conjecture
where previous test found no power-of-two cycles (conjecture holds: False).
Refinements:
- Regular graph construction (all vertices same degree)
- Exhaustive DFS cycle detection
- More samples per n (5 instead of 3)
- Extended n values [8, 10, 12, 14, 16]
Goal: Determine if previous negative result was due to random graph construction
or if regular graphs with exhaustive cycle detection find power-of-two cycles.
Script created: investigate_erdos_gyarfas_refined.py
Execution canceled by user - awaiting further instructions.
