J_bit
plain-language theorem explainer
J_bit defines the per-bit J-cost as the natural logarithm of the golden ratio. Astrophysicists deriving observability limits for stellar systems cite this when bounding photon flux against recognition thresholds in coherence volumes. It supplies the logarithmic term in total J-cost minimization under the module's flux and assembly constraints. The definition is a direct assignment that records equality to Mathlib's goldenRatio via the upstream Constants bundle.
Claim. Let $J$ denote the J-cost function and let $phi$ be the golden ratio. Define $J_{bit} := ln phi$.
background
The module develops Strategy 3 for recognition-bounded observability. Observable flux must satisfy F greater than or equal to E_coh over tau_0 while mass assembly is limited to coherence volume V approximately l_rec cubed. The optimal configuration minimizes total J-cost given by J_total equals J_mass of M plus J_light of L, which produces M/L ratios in the set of phi to the power n for n in zero to three.
proof idea
Direct noncomputable definition that assigns Real.log phi. The attached comment records that Constants.phi coincides with Mathlib's goldenRatio.
why it matters
J_bit supplies the bit-cost term that enters J_total minimization in the observability module. It supports the main result that M/L lies in the set of phi powers and aligns with the phi fixed point and J-cost accounting from the Recognition framework. The definition depends on the Constants structure that bundles Knet, Cproj, Ceng, Cdisp with the nonnegativity hypothesis on Knet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.