J_bit_pos
plain-language theorem explainer
The lemma establishes that the elementary ledger bit cost J_bit equals ln φ and is strictly positive. Astrophysicists deriving stellar mass-to-light ratios from recognition cost differentials during collapse cite this result to guarantee positive increments along the phi-ladder. The proof is a one-line term-mode wrapper that unfolds the definition of J_bit and applies the standard fact that the natural logarithm is positive for arguments exceeding one, using the prior lemma one_lt_phi.
Claim. $0 < J_{bit}$ where $J_{bit} := ln φ$ and $φ = (1 + √5)/2 > 1$ is the golden ratio.
background
The StellarAssembly module derives stellar mass-to-light ratios from recognition cost differentials between photon emission and mass storage during collapse. The core cost function is J(x) = ½(x + 1/x) - 1, and J_bit is defined as the elementary unit J_bit = Real.log φ. This positivity result ensures that cost increments n · J_bit remain positive when partitioning ticks on the phi-ladder, consistent with the module's claim that M/L lies in {φ^n : n ∈ [0,3]}.
proof idea
The term proof unfolds J_bit to Real.log φ and applies Real.log_pos directly to the upstream lemma one_lt_phi : 1 < φ. No additional tactics or reductions are required.
why it matters
This lemma supplies the positivity step required by PlanckScaleMatching.extremum_condition, lambda_rec_from_Jbit_pos, and planck_scale_matching_cert, as well as by ConstantDerivations.J_bit_pos and PhiForcing.J_bit_pos. It closes the elementary positivity gap in the recognition cost model for stellar assembly, linking directly to the T5 J-uniqueness and the eight-tick octave in the forcing chain. No open scaffolding remains for this specific claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.