combFrequencyGM
plain-language theorem explainer
The Schwarzschild absorption-comb kernel is the exact real number ln(φ)/(8π) ≈ 0.019147 in geometric units. Horizon-thermodynamics and RS gravity workers cite it as the headline dimensionless frequency of the φ-area-gap model. It is a pure definition (no proof obligations), packaging the first-law conversion of a putative area step ΔA = 4 ln(φ) ℓ_P² into a mass/frequency step.
Claim. Define the dimensionless Schwarzschild comb frequency by $GM\cdot\omega^* := \frac{\ln\varphi}{8\pi}$, where $\varphi$ is the golden ratio (RS self-similar fixed point). This is the exact algebraic value of the model absorption comb for a Schwarzschild hole in units $\hbar=c=1$.
background
This module is a falsifier-gated preflight of a MODEL mechanism for Pillar 3, not a prediction. The candidate story is horizon-area quantization with gap $\Delta A = 4\ln\varphi,\ell_P^2$, converted by black-hole thermodynamics into a repeated absorption comb at $GM\omega^* = \ln\varphi/(8\pi)$ for Schwarzschild. The module explicitly separates this absorption/level-structure claim from the dead $\varphi$-rung echo-train route.
Existing capital supplies continuous horizon area $A=4\pi R_s^2$, a real-valued ledger capacity bound, and a recognition ledger with boundary cost; none of these force a discrete area spectrum. The first law $\Delta M = \kappa,\Delta A/(8\pi)$ with $\omega=\Delta M$ (and $\kappa=1/(4GM)$ for Schwarzschild) is the algebraic bridge that turns a model area step into this frequency kernel.
The only upstream dependency is the constants bundle that exposes $\varphi$. Numerics for the decimal window live downstream.
proof idea
One-line definitional abbreviation: the real is Real.log Constants.phi divided by 8 * Real.pi. No tactics, no lemmas, no obligations. Downstream positivity and interval theorems unfold this def and apply log-positivity or certified log-$\varphi$ and $\pi$ bounds.
why it matters
This is the named kernel constant for the whole preflight. Downstream, combFrequencyGM_pos records positivity, and combFrequencyGM_bounds pins the decimal window $0.0191 < \ln\varphi/(8\pi) < 0.0193$ (true value $\approx 0.019147$). The headline identity schwarzschild_comb_frequency shows that under the inserted model hypotheses (surface gravity $\kappa=1/(4GM)$ and area gap $4\ln\varphi,\ell_P^2$), the transition frequency collapses exactly to this constant. kerrCombOffset_eq checks consistency: the Kerr offset is $4\kappa$ times the same kernel, recovering the Schwarzschild case when $\kappa=1/(4GM)$.
In the RS map this sits under gravity/Pillar 3, not under the sealed T0–T8 forcing chain. The doc-comment marks it MODEL tier: a consequence of an underived area-quantization hypothesis via the first law, not a prediction until that quantization is derived. The module status remains open; P1 scaling falsifiers already block a uniform ledger gap at the current formalization level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.