schwarzschild_comb_frequency
plain-language theorem explainer
For Schwarzschild parameters the model absorption comb sits exactly at $GM\cdot\omega^*=\ln\varphi/(8\pi)$. Anyone quoting the headline observable of the $\varphi$-horizon absorption mechanism cites this identity. The proof is pure field algebra after unfolding the model transition frequency and the comb constant; no dynamics enter.
Claim. Let $G,M,\ell_P^2\in\mathbb{R}$ be nonzero. With surface gravity $\kappa=1/(4GM)$ and model area gap $\Delta A=4\ln\varphi\cdot\ell_P^2$, the product $(GM)\cdot\omega_{\mathrm{model}}(\kappa,\ell_P^2,\Delta A)$ equals the fixed comb value $\ln\varphi/(8\pi)$.
background
This module is a falsifier-gated preflight of a MODEL mechanism for a $\varphi$-horizon absorption comb, not a prediction. The candidate inserts an area gap $\Delta A=4\ln\varphi\cdot\ell_P^2$ and converts it, via black-hole thermodynamics, into a repeated transition-frequency comb. For Schwarzschild the surface gravity is $\kappa=1/(4GM)$; the model transition frequency is the kinematic map from $(\kappa,\ell_P^2,\Delta A)$ to an angular frequency $\omega^*$.
The sealed BlackHoleEntropy capital supplies only continuous horizon area $A=4\pi R_s^2$ and a real capacity bound $A/\ell_0^2$; neither quantizes area. RecognitionLedger supplies a real-valued boundary cost on a bipartition, again with no spectrum. The present identity therefore lives entirely inside the inserted model hypotheses.
The numeric target is $GM\omega^*=\ln\varphi/(8\pi)\approx 0.019147$. This is an absorption/level-structure claim, categorically distinct from the dead $\varphi$-rung echo-train route (damping $1/\varphi$) already ruled out by O3/O4.
proof idea
Term-mode algebra. Unfold modelTransitionFrequency and combFrequencyGM by definitional rewrite, record $\pi\neq 0$, then field_simp clears the rational expression in $G$, $M$, $\ell_P^2$, $\ln\varphi$, and $\pi$. The nonzero hypotheses on $G$, $M$, and $\ell_P^2$ discharge the denominators. No external lemma beyond $\pi\neq 0$ is required.
why it matters
This is the mechanism's headline observable: once the model gap and Schwarzschild $\kappa$ are inserted, the comb locks at $\ln\varphi/(8\pi)$ with no free parameter. Downstream it is referenced in the vicinity of AreaGapTarget, the still-open P3 demand that $A(n+1)-A(n)=4\ln\varphi\cdot\ell_P^2$ hold exactly for every level, not merely asymptotically.
Within the Recognition framework the identity is kernel-checked kinematics only. Pillar 3 remains open: quantization is not forced by RS capital, and the P1 scaling falsifiers (scaling_family_blocks_ledger_gap, ledger_boundary_cost_no_uniform_gap) already block a uniform ledger gap under continuous rescaling. The result therefore measures what the model algebra forces, and nothing more; it does not close the seven-gaps gravity program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.