J_bit
plain-language theorem explainer
J_bit defines the per-bit information cost in Recognition Science units as the natural logarithm of the golden ratio phi. Researchers modeling nucleosynthesis via discrete phi-tiers cite it when computing mass-to-light ratios from nuclear density and luminosity scalings. The declaration is a direct noncomputable assignment using Real.log on the imported phi constant.
Claim. Let $J_{bit} := log φ$, where $φ$ is the golden ratio serving as the self-similar fixed point.
background
The module derives mass-to-light ratios from discrete φ-tier structures. Nuclear density scales as φ to an integer power times Planck density; photon luminosity follows a parallel φ-power law. Their ratio equals φ to the tier difference. The eight-tick cycle constrains reactions to phase-locked windows and forces integer Δn. J_bit supplies the logarithmic measure of one tier step. Upstream, the phi constant rests on lemmas from PhiSupport while IntegrationGap.A fixes the active edge count per tick at 1.
proof idea
Direct definition. It assigns Real.log φ to J_bit with no lemmas, tactics, or reductions applied.
why it matters
The definition anchors tier-difference calculations that produce M/L ratios in the set {φ^n : n ∈ [0,3]}. It instantiates the self-similar fixed point phi (T6) and supports the eight-tick octave periodicity (T7) that governs nucleosynthesis windows. The module states this matches Strategy 1 results with typical value ≈ φ^1. No downstream uses appear yet, leaving open its integration into stellar assembly or luminosity tier models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.