Brandon Schneider 1872b69ba7 feat(physics): DESI invariant and 16D horn-fiber model projection ... Add two Lean modules projecting the Menger/Koch/Gabriel-Horn fiber model onto DESI DR2 cosmological observables: - DESIInvariant.lean: Hardcoded DESI DR1/DR2 constants as Q16_16 Int literals. Zero Float arithmetic. 7 observational parameters + sigma bounds. 5 native_decide theorems. 7 eval! receipts. - DESIModelProjection.lean: Maps 16D model predictions onto DESI observables. 4-component residual computation with verdict classification. 17 native_decide theorems proving: * All 4 observables within 1s of DESI DR2 * Directional agreement on w0 > -1, wa < 0 * Menger/Koch geometric facts (d_H < 3, D_K < d_H, divergence > 1) * Horn volume bounded, surface grows, torsion drives boundary Receipt: desi_model_projection_receipt_2026-05-13.md Build: lake build Semantics 3529 jobs, zero errors		2026-05-13 20:21:18 -05:00
..
blockchain_corpus	Add NUVMAP scan scheduling receipts	2026-05-11 14:49:17 -05:00
stack_solidification	feat(physics): DESI invariant and 16D horn-fiber model projection	2026-05-13 20:21:18 -05:00