PlanckConstantCert
plain-language theorem explainer
PlanckConstantCert packages the fixed coherence exponent at 5 with positivity of the RS-derived constants hbar_RS, G_RS, kappa_RS and the Einstein relation kappa_RS = 8 pi G_RS. Researchers deriving SM constants from the Recognition Science forcing chain cite this structure when instantiating the native values for Planck's constant and Newton's gravitational constant. The declaration is a structure definition that directly assembles the exponent equality from CoherenceExponentUniqueness with positivity lemmas imported from Constants.
Claim. The structure PlanckConstantCert asserts that the coherence exponent equals 5, that the RS Planck constant satisfies $0 < hbar_RS$, that $0 < G_RS$, that $0 < kappa_RS$, and that the Einstein relation $kappa_RS = 8 pi G_RS$ holds, where $G_RS = phi^5 / pi$ and $hbar_RS = phi^{-5}$.
background
The module certifies the RS-native constants once the coherence exponent is fixed at 5. From the module documentation, k=5 is forced at D=3 by the Fibonacci route k_fib(D)=2^D - D =5 and the integration route k_int(D)=D+2=5. The referenced definition G_RS states G = phi^5 / pi in RS units. Upstream, CoherenceExponentUniqueness supplies the definition coherenceExponent :=5, while Constants supplies the positivity lemmas hbar_pos and G_pos that are lifted to the RS versions.
proof idea
This is a structure definition that collects the fixed exponent equality coherenceExponent =5 together with the positivity statements hbar_RS_pos, G_RS_pos, kappa_RS_pos and the Einstein relation. It serves as a packaging definition for downstream use in planckConstantCert.
why it matters
This structure supplies the certified RS values for the Planck constant and gravitational constant that feed directly into the planckConstantCert definition. It realizes the module goal of certifying hbar = phi^{-5} and G = phi^5 / pi in RS units once the coherence exponent is pinned at 5 by the uniqueness theorem. In the framework this closes the derivation of the fundamental constants from the eight-tick octave and D=3 forcing, with k=5 obtained via the Fibonacci or integration routes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.