oscCost_forces_unit_weight
plain-language theorem explainer
If a real scalar multiplies the oscillatory RCL solution and the product still obeys the Recognition Composition Law, the scalar is 0 or 1. Constraint-sector auditors cite this to show unit-weight forcing is blind to recognition content: a non-cost works the same way. Proof is a short application of the generic forcing lemma, with nonzeroness discharged at exp(π).
Claim. Let $\mathrm{osc}_1$ be the oscillatory solution of the Recognition Composition Law. If $w\in\mathbb{R}$ is such that $x\mapsto w\,\mathrm{osc}_1(x)$ satisfies $G(xy)+G(x/y)=2G(x)G(y)+2G(x)+2G(y)$ for all $x,y>0$, then $w=0$ or $w=1$.
background
The Recognition Composition Law (RCL) is the functional equation $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ on positive reals. In the constraint-sector kinetic derivation, unit kinetic weight is forced by requiring that a scaled cost still obey RCL. This module runs the reparametrization attack: if the same unit-weight conclusion holds for functionals that are not the recognition cost $J$, the forcing step is not reading recognition content.
The oscillatory cost is one such non-$J$ RCL solution (alongside power reparametrizations $x\mapsto J(x^n)$). It is bounded and admits no chart identity of the $J\log$ form. The upstream generic lemma already shows that any $F$ satisfying RCL and nonzero at some positive point forces $w\in{0,1}$ for scaled maps $w\cdot F$; the mechanism is quadraticity of the law in $F$, giving $w^2=w$ on the quadratic term.
Local setting is Campaign 2 Track A against the paper claim that field-independence of the kinetic weight extracts recognition content from RCL alone.
proof idea
Apply the generic unit-weight forcing lemma to $F=\mathrm{osc}_1$ and the given weight $w$. Supply: $\mathrm{osc}_1$ itself satisfies RCL; the scaled map satisfies RCL (hypothesis); and $F$ is nonzero somewhere. Witness the last at $x=\exp(\pi)>0$ via positivity of the exponential, rewrite $F(\exp(\pi))$ by the known negative evaluation of the oscillator there, and finish with a numeric check. The generic lemma returns $w=0\lor w=1$.
why it matters
Feeds the parent package that constraint-sector recognition load is quadraticity of RCL, not unit weight: the parent pairs this oscillatory case with the power-cost orbit to show the solution set of RCL is large enough that "$w\cdot F$ obeys RCL $\Rightarrow w\in{0,1}$" holds for non-costs. The paper's stated reason to expect the attack to fail (conclusion is a functional form, not a level set) is answered: the attack lands, at lower severity than the O5 ladder attack, but the recognition-load claim for unit weight still fails.
Framework landmark: RCL itself (the composition law behind T5 $J$-uniqueness). The unit-weight step never reaches $J$-uniqueness; it only uses that the law is quadratic in the unknown functional. Downstream commentary stresses the complementary point: the oscillator is bounded and cannot supply the chart identity that earns $J$ its place in the model class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.