N_horizon_pos
plain-language theorem explainer
Black-hole entropy derivations in Recognition Science cite N_horizon_pos to guarantee that the combinatorial microstate count remains positive for any nonnegative horizon area A. The result ensures the expression 2 raised to the patch count is strictly positive before taking logarithms. The proof is a term-mode one-liner that unfolds the definition and applies the general positivity of real exponentiation with positive base.
Claim. For every real number $A$ with $A$ nonnegative, the horizon microstate count $N(A) = 2^{A/4}$ satisfies $N(A) > 0$.
background
The module derives black-hole horizon states from the discrete Q3 ledger. The horizon of area A in Planck units supports A/4 admissible Q3-orbit patches; each patch is a 2-cell under the SU(2) projection of Q3 and therefore carries two microstates. This produces the definition N_horizon(A) equal to 2 raised to the horizon patch count, which equals 2 to the power A/4 in the leading term.
proof idea
The proof is a term-mode one-liner. It unfolds N_horizon to expose the real exponentiation with base 2, then applies Real.rpow_pos_of_pos. The base positivity 2 > 0 is discharged by norm_num.
why it matters
N_horizon_pos supplies one of the five clauses collected in the BlackHoleHorizonStatesCert structure. It is invoked inside the one-statement packaging theorem black_hole_horizon_states_one_statement together with the log-bridge equality S_lead log 2 = log N_horizon and the c_RS band result. Within the Recognition framework the positivity step closes the combinatorial counting argument that replaces the asserted Bekenstein-Hawking prefactor with an explicit ledger count, consistent with the phi-ladder and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.