kerrCombOffset
plain-language theorem explainer
Defines the Kerr locked-comb offset at surface gravity κ as κ·ln(φ)/(2π): the frequency shift of absorption lines from the superradiant bound. Anyone checking the Kerr extension of the Schwarzschild GMω* comb cites this. It is a pure definitional abbreviation of that closed-form expression.
Claim. For surface gravity $\kappa\in\mathbb{R}$, the Kerr comb offset is $\kappa\,\ln(\varphi)/(2\pi)$, where $\varphi$ is the golden ratio fixed by the RS self-similarity condition.
background
This module is a falsifier-gated preflight of a MODEL horizon absorption mechanism, not a prediction. The candidate story is area quantization with gap $\Delta A=4\ln(\varphi),\ell_P^2$, converted by black-hole thermodynamics into a repeated absorption comb. For Schwarzschild the dimensionless marker is $GM\omega^*=\ln(\varphi)/(8\pi)\approx 0.019147$. Pillar 3 remains open: kinematic algebra is real, quantization itself is not forced from RS capital.
The present definition packages the Kerr form of that offset. In Kerr, absorption lines sit at a fixed offset from the superradiant bound $\omega-m\Omega_H$, with the offset proportional to surface gravity $\kappa$. The constant of proportionality is $\ln(\varphi)/(2\pi)$, so the full offset is $\kappa\ln(\varphi)/(2\pi)$. This is categorically an absorption/level-structure claim, not the dead $\varphi$-rung echo-train route (damping $1/\varphi$).
Upstream capital used nearby includes the continuous horizon-area mirror $A=4\pi R_s^2$, ledger capacity bounds, and recognition-ledger boundary cost; none of those objects quantize area. $\varphi$ enters only as the RS fixed point already present in Constants.
proof idea
Definitional one-liner: return $\kappa\cdot\log\varphi/(2\pi)$. No lemmas, no tactics. Downstream equalities rewrite this name against combFrequencyGM or modelTransitionFrequency and finish by field simplification and ring.
why it matters
Gives a single named handle for the Kerr comb offset so the preflight can state two kernel checks cleanly. kerrCombOffset_eq proves consistency with the Schwarzschild observable: the Kerr offset equals $4\kappa$ times combFrequencyGM, and the Schwarzschild surface gravity $\kappa=1/(4GM)$ recovers $GM\omega^*=\ln(\varphi)/(8\pi)$. model_area_gap_gives_kerr_comb shows that feeding the MODEL gap $\Delta A=4\ln(\varphi),\ell_P^2$ through the first-law conversion yields exactly this offset.
In the Seven Gaps map this is Tier MODEL on the same underived chain: the algebra is sealed, the quantization hypothesis is not. It does not revive the killed echo discriminator; it only organizes the absorption-comb side of Pillar 3 preflight. Framework landmarks touched are $\varphi$ (T6 fixed point) and the $\ln(\varphi)$ factor that would appear if an area gap of that form were ever forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.