bhCoefficient_pos
plain-language theorem explainer
The theorem establishes positivity of the Bekenstein-Hawking coefficient. Workers formalizing entropy bounds in holographic dualities cite it to fix the canonical factor. The proof is a one-line wrapper that unfolds the constant definition and normalizes the numerical inequality.
Claim. The Bekenstein-Hawking coefficient satisfies $0 < 1/4$.
background
The module encodes the holographic principle from Recognition Science by packaging five duality contexts of dimension five together with the entropy bound. The Bekenstein-Hawking coefficient is defined as the constant 1/4 that appears in the area-entropy relation. This positivity theorem supplies one field of the downstream holographic certificate.
proof idea
The proof is a one-line wrapper. It unfolds the definition of the Bekenstein-Hawking coefficient to the constant 1/4 and applies norm_num to verify the strict inequality.
why it matters
The result supplies the bh_coeff_pos field required by the holographicCert definition, which bundles the count of duality contexts with coefficient positivity. It anchors the structural capture of the entropy bound S ≤ A/4 inside the Recognition Science treatment of holography. The module reports zero sorrys and zero axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.