combFrequencyGM_pos
plain-language theorem explainer
The dimensionless Schwarzschild absorption-comb frequency ln(φ)/(8π) is strictly positive. Anyone working the horizon-ledger preflight or the candidate φ-area gap model needs this sign fact before quoting interval bounds. The proof is a one-line term: log-positivity from φ > 1, divided by a positive 8π denominator.
Claim. The comb frequency $GM\omega_*=\ln\varphi/(8\pi)$ satisfies $0<GM\omega_*$, where $\varphi=(1+\sqrt{5})/2$ is the golden ratio forced by the Recognition self-similarity fixed point.
background
This module is a falsifier-gated preflight of a model mechanism for Pillar 3 (gravity), not a prediction. The candidate claims horizon-area quantization with gap $\Delta A=4\ln\varphi,\ell_P^2$, which black-hole thermodynamics converts into a repeated absorption comb at $GM\omega_*=\ln\varphi/(8\pi)\approx 0.019147$ for Schwarzschild. That quantity is the comb frequency named here.
The golden ratio $\varphi$ enters from the RS forcing chain (T6): it is the unique self-similar fixed point of the cost calculus, and $\varphi>1$ is elementary. The Recognition ledger capital supplies real-valued boundary costs and capacity bounds, not a discrete area spectrum; quantization itself is not forced by existing capital.
Upstream, Constants.one_lt_phi records $1<\varphi$. The nearby kernel-interval comment pins $0.0191<\ln\varphi/(8\pi)<0.0193$ via Taylor-certified log-$\varphi$ bounds and decimal $\pi$ inequalities, with an explicit trust-base caveat on native_decide.
proof idea
One-line term proof. Apply div_pos to the quotient $\ln\varphi/(8\pi)$: the numerator is positive by Real.log_pos on Constants.one_lt_phi ($1<\varphi$ implies $\ln\varphi>0$), and the denominator $8\pi$ is discharged by positivity. No further lemmas are needed.
why it matters
Positivity is the first kinematic sanity check on the absorption-comb observable before any numerical window or ledger comparison. The module status is explicit: Pillar 3 stays open; nothing here predicts. The load-bearing quantization hypothesis is not derived from RS capital, and sibling results (scaling_family_blocks_ledger_gap, ledger_boundary_cost_no_uniform_gap) already record that the P1 scaling falsifier blocks a uniform ledger gap at the current formalization level.
This fact sits upstream of the kernel interval $0.0191<GM\omega_*<0.0193$ and of any later comparison against horizon-area or boundary-cost mirrors. It does not revive the dead $0.618$ echo-train discriminator; the observable is an absorption/level-structure comb, categorically distinct from O3/O4 echo bounds. Framework landmarks in play are T6 ($\varphi$ forced) and the continuous horizon-area/ledger-capacity capital, not T7/T8 or the RCL identity directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.