J_bit_normalized
plain-language theorem explainer
The normalized bit cost of one recognition event is fixed at unity in RS-native dimensionless units. Derivations of the recognition length λ_rec from curvature balance and the subsequent definition of G cite this normalization as the fixed left-hand side of the cost equation. It is introduced directly as a constant definition with no further reduction or lemmas.
Claim. The normalized bit cost of a single recognition event is defined by $J_{bit} = 1$.
background
The LambdaRecDerivation module derives λ_rec non-circularly by balancing the bit cost against the curvature cost J_curv(λ) = 2λ². The curvature cost follows from a ±4 curvature packet on the 8 vertices of Q3, Gauss-Bonnet normalization on S² (χ = 2), and bounding area 4πλ², yielding J_curv λ = 2λ² as stated in both the local J_curv definition and the upstream PlanckScaleMatching version. The module documentation fixes the bit cost at 1 in these units so that G emerges as π λ_rec² c³ / ℏ once the balance condition is solved.
proof idea
Direct definition that sets the constant J_bit_normalized to 1. No lemmas or tactics are invoked; the value is the normalization convention stated in the module documentation.
why it matters
This supplies the constant term in the balance residual used by balance_at_lambda_0, balance_determines_lambda, balance_unique_positive_root, and the GDerivationChain structure. The chain records the steps from Q3 combinatorics through Gauss-Bonnet to the formula for G, implementing the T5 J-uniqueness condition by anchoring the bit cost at unity so that the self-similar fixed point fixes the scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.