J_bit_eq_phi_minus
plain-language theorem explainer
The equality fixes the bit cost J_bit exactly as phi minus three halves at the golden ratio scale. Workers deriving the recognition wavelength from ledger-curvature equilibrium cite it to obtain the precise starting value for J_bit. The proof reduces the expression by first establishing the reciprocal identity from the quadratic relation for phi then applying ring normalization.
Claim. $J(phi) = phi - 3/2$, where $J(x) := (x + x^{-1})/2 - 1$ and the identity $phi^{-1} = phi - 1$ follows from $phi^2 = phi + 1$.
background
The module derives lambda_rec approximately 0.564 Planck lengths by equating bit cost to curvature cost at equilibrium for conjecture C8. J_bit_val is the evaluation of the cost functional J at the golden ratio phi, equivalently written as cosh(ln phi) minus one. The upstream lemma phi_sq_eq supplies the defining quadratic identity phi squared equals phi plus one.
proof idea
The tactic proof unfolds J_bit_val and J. It proves the auxiliary fact phi inverse equals phi minus one by rewriting phi squared equals phi plus one, applying field_simp, and closing with linarith. Substitution followed by ring then yields the goal.
why it matters
The result supplies the exact algebraic form invoked by the downstream numerical bounds theorem J_bit_bounds. It completes the bit-cost step in the derivation chain for conjecture C8 of the Discrete Informational Framework Paper, connecting the self-similar fixed point phi to the ledger transition cost that enters the extremum condition for the recognition scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.