phiClosed_one_div_pow

In RecogSpec.Core, a real $x$ is $\varphi$-closed when $x\in\mathrm{phiSubfield}(\varphi)$, the subfield of $\mathbb{R}$ generated by $\varphi$ under the field operations. The predicate is the membership gate used throughout the dimensionless pack: every displayed constant or ratio must be algebraic over $\varphi$ in this sense.

Core already records that the predicate is a subfield: it contains $1$, is closed under powers of $\varphi$ itself ($\varphi^n$ is $\varphi$-closed), and is closed under division. Those three facts are the only upstream inputs here.

The local setting is the Recognition Spec layer that assembles calibrated anchors, band constraints, and the universal dimensionless pack before verification certificates consume them.

Term-mode, three steps. First, unit closure gives that $1$ is $\varphi$-closed. Second, self-power closure gives that $\varphi^n$ is $\varphi$-closed. Third, apply the Core division lemma: the quotient of two $\varphi$-closed reals is $\varphi$-closed, yielding $1/\varphi^n$.

Inverse powers of $\varphi$ appear throughout Recognition Science native units (for example $\hbar=\varphi^{-5}$ and the Berry threshold $\varphi^{-1}$). This lemma is the elementary gate that puts those terms inside the $\varphi$-subfield.

It is consumed by the explicit universal dimensionless pack constructor and by HonestClosureCert, whose Part A requires that all observables be $\varphi$-closed. Without inverse-power closure, the pack and the honest-closure witness cannot discharge the algebraic side of the certificate.

The result is pure field arithmetic; it does not touch the forcing chain T5–T8, but it is infrastructure those later numerical claims rely on once $\varphi$ is fixed.