J_bit_bounds
plain-language theorem explainer
The theorem establishes that the bit cost J(φ) lies strictly between 0.11 and 0.12 when φ is the golden ratio. Researchers deriving the recognition wavelength from ledger-curvature matching cite this interval to confirm numerical consistency with the self-similar scale. The proof rewrites J_bit_val via the exact identity J(φ) = φ - 3/2 and applies linear arithmetic to the supplied bounds 1.61 < φ < 1.62.
Claim. $0.11 < J(φ) < 0.12$, where $J(x) = (x + x^{-1})/2 - 1$ and φ is the golden ratio.
background
The PlanckScaleMatching module derives λ_rec ≈ 0.564 ℓ_P by equating the bit cost J_bit to a curvature cost extracted from Q₃ geometry. The bit cost is defined as J_bit_val := J(φ), where the J-functional is the unique cost satisfying the Recognition Composition Law and evaluates to cosh(ln φ) - 1 at the self-similar fixed point φ. This supplies the left-hand side of the extremum condition J_bit = J_curv(λ) = 2λ² in RS-native units (c = 1, ħ = φ^{-5}).
proof idea
The proof is a one-line wrapper that first rewrites J_bit_val to φ - 3/2 via the algebraic identity J_bit_eq_phi_minus. It then splits the conjunction and invokes linarith on the lower bound using phi_gt_onePointSixOne together with the upper bound using phi_lt_onePointSixTwo.
why it matters
This bound supplies the J_bit_numerical field of the PlanckScaleMatchingCert, which certifies the full chain for Conjecture C8. It anchors the numerical value of the ledger bit cost inside the interval required for the subsequent face-averaging step that introduces the factor 1/π and produces the Planck ratio λ_rec / ℓ_P = 1/√π. The result closes the consistency check between the T5 J-uniqueness and the D = 3 geometry in the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.