kappa_RS_pos
plain-language theorem explainer
Positivity of the RS-native gravitational coupling κ_RS = 8 φ^5 follows from φ > 0 and the coherence exponent fixed at 5. Researchers verifying RS-derived constants against the Einstein relation would cite this when assembling the PlanckConstantCert structure. The proof is a term-mode multiplication of the positive numeral 8 and the positive power φ^5.
Claim. $0 < 8 φ^5$ in RS-native units, where φ denotes the golden ratio and the exponent 5 is the coherence value forced by D = 3.
background
The module certifies RS-native constants once the coherence exponent is fixed at 5. Upstream, CoherenceExponentUniqueness establishes k = 5 via two routes (Fibonacci and integration) that both yield 5 at D = 3. This pins ħ = φ^{-5} and G = φ^5 / π, after which κ_RS is set to 8 φ^5 to match the structural Einstein relation κ = 8πG. The J-cost reparametrization G(t) = cosh(t) - 1 supplies the underlying functional equation but is not invoked in the positivity argument.
proof idea
Term proof applies mul_pos to the constant 8 (discharged by norm_num) and the power φ raised to the coherence exponent (discharged by pow_pos). No additional lemmas or hypotheses are required.
why it matters
The result supplies the kappa_pos field required by planckConstantCert, which bundles the full set of RS constants and the Einstein relation. It closes the algebraic verification step that follows the forcing chain (T5–T8) once k = 5 is established. The declaration touches the open question of unit conversion to SI values but provides the necessary positivity for the certification to be well-formed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.