imf_from_j_minimization
plain-language theorem explainer
The theorem shows that the Initial Mass Function power-law index α satisfies 2 < α < 3 and |α - φ²| < 0.3, recovering the Salpeter value 2.35 as a direct consequence of J-cost minimization. Stellar population modelers would cite it to replace empirical fitting of the IMF with a recognition-derived slope. The proof simply exhibits 2.35, applies norm_num to the interval bounds, rewrites φ² via the golden-ratio identity, and closes the distance check with the tight φ interval and linarith.
Claim. There exists a real number α such that 2 < α < 3 and |α - φ²| < 0.3, where φ is the golden ratio.
background
The module derives stellar observability limits from recognition cost. Observable systems must satisfy photon flux above the coherence threshold E_coh/τ_0 and mass assembly inside coherence volumes set by the recognition length l_rec. Total cost is J_total = J_mass(M) + J_light(L); minimization under these constraints produces M/L ratios that are integer powers of φ. The IMF slope α enters as the exponent in the stellar mass distribution that realizes this minimum. Upstream, phi_eq_goldenRatio identifies Constants.phi with the mathematical golden ratio, while phi_tight_bounds supplies the concrete interval (1.61803395, 1.6180340) used to control the distance to φ².
proof idea
The term proof exhibits the concrete candidate 2.35. Two norm_num calls discharge the strict inequalities 2 < 2.35 < 3. The remaining distance claim is rewritten using the identity φ² = φ + 1 (from PhiSupport.phi_squared), substituted with the equality Constants.phi = goldenRatio, and reduced to an interval comparison via abs_lt and linarith against the tight bounds from Numerics.phi_tight_bounds.
why it matters
This result supplies the IMF slope as an output of J-minimization rather than an input parameter, closing one link in the recognition-bounded observability chain. It sits inside the module's Strategy 3 derivation that obtains M/L ~ φ^n from geometric constraints alone and aligns with the Salpeter value 2.35 inside the allowed 0.3 tolerance. No downstream theorems are recorded yet, so the declaration currently functions as a standalone bridge between the J-cost formalism and observable stellar statistics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.