GDerivationChain
plain-language theorem explainer
GDerivationChain bundles the six-step certificate deriving Newton's G and Einstein kappa from Q3 cube geometry plus normalized bit cost. Researchers tracing constants in recognition-based gravity cite it to confirm the non-circular path from curvature normalization to G = lambda_rec squared c cubed over pi hbar. The structure is assembled by direct substitution of proved equalities from sibling lemmas on J_curv and balance uniqueness.
Claim. A structure asserting that the cube Q_3 has 8 vertices, that Q_3 vertices times angular deficit per vertex equals 2 pi times the Euler characteristic of S^2, that the curvature cost satisfies J_curv(lambda) = 2 lambda^2 for all lambda, that there exists a unique positive lambda balancing J_curv(lambda) with the normalized bit cost 1, that G = lambda_rec^2 c^3 / (pi hbar), and that kappa = 8 phi^5.
background
The LambdaRecDerivation module derives the recognition length lambda_rec non-circularly from the bit cost normalized to 1 and the curvature cost J_curv(lambda) = 2 lambda^2 obtained via Gauss-Bonnet on the Q3 cube. G is then defined as the consequence lambda_rec^2 c^3 / (pi hbar), and kappa_einstein follows as 8 pi G / c^4 which reduces to 8 phi^5 once hbar = phi^{-5}. Q3_vertices fixes the cube vertex count at 8. J_curv is the curvature cost of embedding one recognition token at scale lambda, obtained from four curvature quanta, chi = 2 on S^2, and bounding area 4 pi lambda^2. J_bit_normalized sets the bit cost to 1. This rests on the upstream lambda_rec definition from Bridge.DataCore as sqrt(hbar G / (pi c^3)) together with the constants module expressions for G, hbar, and kappa.
proof idea
The structure is defined by enumerating its six fields. Each field is instantiated by direct reference to a proved fact: step1 by the definition Q3_vertices = 8, step3 by the algebraic definition of J_curv, step4 by the uniqueness result balance_unique_positive_root, and steps 5-6 by the constant definitions in the Constants module. The complete instantiation with explicit proofs for each step appears in the downstream theorem G_derivation_chain_complete.
why it matters
This structure supplies the certificate that the derivation of G and kappa from recognition costs is complete and non-circular, feeding directly into the theorem G_derivation_chain_complete. It fills the chain step from Q3 geometry through J-uniqueness (T5) to the forcing of phi and the constants in RS-native units, with G expressed as a consequence rather than an input. The module thereby closes the loop from the eight-tick octave to the Einstein coupling without circularity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.