hbar_rs_pos
plain-language theorem explainer
The declaration establishes positivity of the RS-native reduced Planck constant. Researchers deriving the Bekenstein-Hawking entropy bound from ledger capacity on the integer lattice cite it to confirm the sign of ℏ before invoking Gℏ = 1. The proof is a term-mode reduction that unfolds the definition and applies zpow_pos to the known positivity of phi.
Claim. $0 < hbar_{rs}$ where $hbar_{rs} = phi^{-5}$ in RS natural units.
background
In Recognition Science the reduced Planck constant is fixed at ℏ = φ^{-5} in native units (c = 1, G = φ^5). The module derives the Bekenstein-Hawking bound S = A/4 from the ledger on ℤ³, where each voxel carries one unit of information and boundary information scales as volume^{2/3}. The upstream definition hbar_rs sets hbar_rs := phi ^ (-5 : ℤ) and records the identity Gℏ = 1; the theorem from PrimitiveDistinction supplies the axiom-to-structure map that forces D = 3.
proof idea
The proof is a one-line term-mode wrapper. It unfolds hbar_rs to expose phi ^ (-5) and applies the lemma zpow_pos to the positivity of phi.
why it matters
Positivity of ℏ is required for the physical interpretation of the ledger-derived entropy bound S_BH = A/4 that closes Gap G3. It supports the main results bekenstein_hawking_from_rs and G_hbar_product_eq_one in the same module. The assignment ℏ = φ^{-5} is a direct consequence of the forcing chain T5–T8 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.