Deterministic Build Receipt — 2026-05-13
Lean: v4.30.0-rc2
Build: lake build Semantics — 3529 jobs, 0 errors, 0 warnings
Branch: distilled — ac34c7c0 (pushed to github/distilled)
Gdrive: 3 receipt folders in Research Stack/
Module 1: DESIInvariant.lean
Deterministic Constants (hardcoded Int literals, zero Float)
| Symbol |
Value |
Q16.16 / Raw |
Source |
| w₀ |
-0.890 |
-58327 |
DESI DR2 |
| w_a |
-0.480 |
-31457 |
DESI DR2 |
| w₀ (ΛCDM) |
-1.000 |
-65536 |
Planck ΛCDM |
| H₀ |
68.26 |
6826 (×100) |
DESI DR2 |
| Ω_m |
0.2947 |
19312 |
DESI DR2 |
| σ₈ |
0.808 |
52953 |
DESI DR2 |
| r_d |
147 Mpc |
147 |
DESI DR2 |
Deterministic Theorems (native_decide, decidable)
| Theorem |
Statement |
Result |
w0_above_LCDM |
w0_DR2 > w0_LCDM |
True: -58327 > -65536 ✓ |
wa_below_LCDM |
wa_DR2 < wa_LCDM |
True: -31457 < 0 ✓ |
w0_in_3sigma |
w₀ ∈ [central ± 3σ] |
True ✓ |
wa_in_3sigma |
w_a ∈ [central ± 3σ] |
True ✓ |
omegam_in_3sigma |
Ω_m ∈ [central ± 3σ] |
True ✓ |
Module 2: DESIModelProjection.lean
Deterministic Model Predictions vs DESI DR2
| Observable |
Model Value |
DESI Value |
Q16.16 Residual |
Float Residual |
σ |
Verdict |
| w₀ |
-58327 |
-58327 |
0 |
0.000 |
0σ |
Consistent |
| w_a |
-36045 |
-31457 |
-4588 |
-0.070 |
1.4σ |
Consistent |
| Ω_m |
19005 |
19312 |
-307 |
-0.0047 |
1.7σ |
Consistent |
| σ₈ |
53215 |
52953 |
+262 |
+0.004 |
0.27σ |
Consistent |
Deterministic Geometry Constants
| Constant |
Value |
Q16.16 |
Theorem |
| Menger d_H |
ln(20)/ln(3) = 2.72683 |
178696 |
menger_dim_less_than_3 |
| Koch D_K |
ln(4)/ln(3) = 1.26186 |
82706 |
koch_dim_less_than_menger |
| MK divergence base |
(9/5) = 1.8 |
117964 |
mk_divergence_exceeds_1 |
| Horn surface growth α |
0.007 |
459 |
horn_surface_grows |
| Torsion coupling β |
0.003 |
197 |
torsion_drives_boundary |
Deterministic Directional Theorems
| Theorem |
Meaning |
Result |
model_w0_direction_aligns |
Model + DESI both say w₀ > -1 |
True ✓ |
model_wa_direction_aligns |
Model + DESI both say w_a < 0 |
True ✓ |
Deterministic Residual Theorems
| Theorem | Bound | |residual| | Pass? |
|---------|-------|---------|-------|
| w0_residual_within_1sigma | 0 ≤ 2621 | Yes ✓ |
| wa_residual_within_2sigma | 4588 ≤ 13108 | Yes ✓ |
| wa_residual_within_3sigma | 4588 ≤ 19662 | Yes ✓ |
| omegam_residual_within_1sigma | 307 ≤ 367 | Yes ✓ |
| omegam_residual_within_2sigma | 307 ≤ 734 | Yes ✓ |
| sigma8_residual_within_bound | 262 ≤ 1966 | Yes ✓ |
Module 3: AdjacentCoprimeClassification.lean
Deterministic Example Results
| Example |
Conditions |
Pass? |
Break Point |
| Fibonacci (c₁=1,c₂=1,a₁=1,a₂=2) |
gcd(a₁,a₂)=1 ✓ gcd(a₂,c₂)=1 ✓ gcd(c₁,c₂)=1 ✓ |
PASS |
Never (all gcd=1) |
| Bad (c₁=2,c₂=2,a₁=1,a₂=3) |
gcd(2,2)=2 ≠ 1 FAIL |
FAIL |
n=2: gcd(8,22)=2 |
| Ex3 (c₁=3,c₂=5,a₁=2,a₂=7) |
gcd(2,7)=1 ✓ gcd(7,5)=1 ✓ gcd(3,5)=1 ✓ |
PASS |
Never (all gcd=1) |
| Bad2 (c₁=2,c₂=4,a₁=1,a₂=3) |
gcd(2,4)=2 ≠ 1 FAIL |
FAIL |
n=3: gcd(10,32)=2 |
| Ex5 (c₁=1,c₂=3,a₁=5,a₂=7) |
gcd(5,7)=1 ✓ gcd(7,3)=1 ✓ gcd(1,3)=1 ✓ |
PASS |
Never (all gcd=1) |
Deterministic #eval Outputs
step(1,1,3,5) = 8 ✓
gcd(5, step(1,1,3,5)) = 1 ✓
gcd(5, 3) = 1 ✓
gcd(5, 1) = 1 ✓
Key Theorems (30 total, all native_decide)
All 30 theorems verified by native_decide produce immutable results:
- Fibonacci example: 3 condition theorems + 9 pairwise gcd theorems
- Bad example: 3 condition theorems + 1 break theorem
- Ex3 example: 3 condition theorems + 8 pairwise gcd theorems
- Bad2 example: 3 condition theorems + 1 break theorem
- Ex5 example: 3 condition theorems + 6 pairwise gcd theorems
Determinism Guarantee
Every value in this receipt is:
- A hardcoded Int literal (no Float, no runtime computation)
- Verified by native_decide (compile-time, deterministic)
- Verified by #eval/#eval! (same result every build)
- Within a Lean namespace (no global mutable state)
Total: 3529 build jobs, 0 errors, 0 warnings, 0 sorries
8aa63e6ae8