G_hbar_pos
plain-language theorem explainer
The product of the gravitational constant and reduced Planck constant is strictly positive in Recognition Science units. Researchers deriving quantum-gravity relations from the J-cost functional would cite this to confirm sign consistency of the derived scales. The proof rewrites the product via the Gauss-Bonnet closure and applies positivity.
Claim. $0 < G ħ$, where $G = λ_{rec}^2 c^3 / (π ħ)$ and $ħ = φ^{-5}$ are the Recognition Science expressions for Newton's constant and the reduced Planck constant.
background
The Quantum-Gravity Octave Duality module derives all constants from the single J-cost functional equation. J-cost equals the AM-GM gap: for x > 0, J(x) = (x - 1)^2 / (2x), which is nonnegative and vanishes only at x = 1. In RS-native units (c = 1), the gravitational constant is G = λ_rec² c³ / (π ħ) and the reduced Planck constant is ħ = φ^{-5}. Upstream results from Constants and PhiForcingDerived establish these closed forms from the phi-ladder and the Recognition Composition Law.
proof idea
One-line wrapper that rewrites the product using the Gauss-Bonnet closure lemma (establishing G ħ = 1/π) and then applies the positivity tactic on the resulting positive real.
why it matters
This theorem confirms the positivity required for the Gauss-Bonnet closure G ħ = 1/π in the module's QG-003. It anchors the Planck area result ℓ_P² = 1/π and supports the broader octave duality κ ħ = 8. The result sits inside the T5-T8 forcing chain and the eight-tick period that fixes D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.