kappa_normalized_eq_one
plain-language theorem explainer
The normalized curvature magnitude per vertex-sphere on the recognition cube equals one, as required by Gauss-Bonnet normalization on the bounding sphere. Researchers deriving the recognition length lambda_rec non-circularly from unit bit cost and curvature cost J_curv = 2 lambda^2 cite this to fix the normalization before defining G. The proof is a short algebraic reduction that unfolds the definition, rewrites via the total curvature identity, simplifies the Euler characteristic, and finishes with ring.
Claim. The normalized curvature magnitude per vertex-sphere satisfies $kappa_normalized = 1$, where $kappa_normalized := Q_3 vertices * angular_deficit_per_vertex / (4 pi)$ and the total curvature identity gives $Q_3 vertices * angular_deficit_per_vertex = 4 pi$.
background
The LambdaRecDerivation module derives lambda_rec non-circularly by balancing the normalized bit cost of one against the curvature cost J_curv(lambda) = 2 lambda^2. This J_curv follows from a curvature packet of magnitude 4 distributed over the eight vertices of Q3, normalized via Gauss-Bonnet on the bounding sphere S^2 whose Euler characteristic is 2. The definition kappa_normalized := Q3_vertices * angular_deficit_per_vertex / (4 * Real.pi) therefore measures the curvature per vertex-sphere in units that make the total equal to 4 pi. The upstream theorem total_curvature_gauss_bonnet states that Q3_vertices * angular_deficit_per_vertex = 2 * Real.pi * euler_S2, with euler_S2 defined as 2.
proof idea
The proof unfolds the definition of kappa_normalized, rewrites the product of vertex count and deficit using the total_curvature_gauss_bonnet theorem, simplifies euler_S2 to the constant 2, and reduces the resulting expression to 1 by ring.
why it matters
This result fixes the curvature normalization inside the non-circular lambda_rec derivation of the Constants.LambdaRecDerivation module, allowing G to be defined afterward as pi * lambda_rec^2 * c^3 / hbar. It rests on the curvature packet axiom from PlanckScaleMatching and the Gauss-Bonnet identity for the cube, consistent with the recognition composition law and the eight-tick octave structure. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.