jBit
plain-language theorem explainer
jBit defines the link-penalty cost as the natural logarithm of the golden ratio phi. Researchers analyzing topological constraints and veto mechanisms in Recognition Science cite this constant to bound the cost of each link crossing. The declaration is a direct constant definition extracted from the log-domain J-cost geometry.
Claim. $J_{bit} := ln φ$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module develops the log-domain geometry for the J-cost in the F1 foundation paper. The canonical cost takes the form J(x) = ½(x + x⁻¹) − 1 and satisfies the reciprocal composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Its exponential version is J(e^ε) = cosh(ε) − 1. jBit isolates the minimal positive cost per topological crossing as ln φ, the logarithm of the self-similar fixed point of J.
proof idea
The declaration is a direct noncomputable definition that assigns the real logarithm of phi to jBit. No lemmas or tactics are applied; the value is introduced as the base link-penalty unit.
why it matters
This definition supplies the positive per-crossing cost that drives the master veto theorem finite_capacity_veto, which demonstrates that rigid rotation cannot emerge from finite-energy initial data because infinitely many crossings would exceed any finite budget. It also supports the link-penalty positive result. In the Recognition framework it realizes the base cost unit for T5 J-uniqueness and the eight-tick octave by quantifying the minimal nonzero ledger bit cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.