compositionLaw_forces_unit_weight_is_an_instance
plain-language theorem explainer
If a real weight multiplies the recognition cost J and the product still obeys the Recognition Composition Law, the weight is forced to 0 or 1. Constraint-sector and gravity workers cite this as the J-specialization of the generic unit-weight forcing. The proof is a one-line application of the generic lemma at the single test point (x,y)=(2,2), using that J itself satisfies RCL.
Claim. Let $J(x)=(x+x^{-1})/2-1$. If $w\in\mathbb{R}$ and $F(x)=w\cdot J(x)$ satisfies the Recognition Composition Law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(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. The standard recognition cost is $J(x)=(x+x^{-1})/2-1$ (also written $\cosh(\log x)-1$), forced uniquely in the T5 step of the unified forcing chain. The predicate SatisfiesCompositionLaw packages RCL as a Prop on real functions.
This module runs Campaign 2 Track A: a reparametrization attack on the constraint-sector kinetic-weight argument from HKTKineticFromRecognitionCost §8. That argument claimed field-independence of the kinetic weight from RCL. The paper printed an unrun falsifier: exhibit a weight functional outside RCL that still forces unit weight. The module shows the original §8 proof never used the shape of $J$ beyond three numerical values at one point.
Upstream, the generic lemma states the same $w\in{0,1}$ conclusion for an arbitrary $F$ obeying RCL and nonzero at a test pair. The sibling certificate that $J$ itself obeys RCL supplies the missing hypothesis for the specialization.
proof idea
One-line term wrapper. Apply the generic forcing lemma to $F:=J$ and the given weight $w$, feeding the RCL certificate for $J$ and the hypothesis that $w\cdot J$ obeys RCL. Instantiate the generic test pair at $x=y=2$ (both positive by norm_num) and discharge the nonzero-cost side condition by evaluating $J(2)$ numerically. No further algebra on $J$ is needed; the quadratic-in-$F$ structure that yields $w^2=w$ lives entirely in the generic lemma.
why it matters
This is the repo §8 lemma rewritten as an instance of the generic unit-weight forcing, so the recognition cost is not load-bearing for that step. Downstream it feeds constraint_sector_recognition_load_is_quadraticity_not_unit_weight_holds, which packages the campaign conclusion: the constraint-sector load is the quadraticity of RCL, not a privileged role for $J$.
In framework terms this sits under RCL (the composition law of T5/J-uniqueness) and under the gravity constraint-sector program. The module doc is explicit that the paper's reason to expect the reparam attack to fail was wrong: §8's conclusion is invariant under a nontrivial monoid action ($x\mapsto x^n$) that moves $J$ while staying inside the solution set. Severity is lower than the O5 ladder attack, but the invariance test demanded by Campaign 1 fails here. The declaration closes the specialization gap so the generic attack can be stated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.