CalibratedWeightAtTwo
plain-language theorem explainer
One-point normalization of a real weight w: the weighted recognition cost equals the bare cost at the single argument 2. Gravity and constraint-sector auditors cite it as a non-RCL witness that still forces unit weight. It is a bare definitional predicate, not a derived theorem.
Claim. A real number $w$ is a calibrated weight at two when $w \cdot J(2) = J(2)$, where $J(x) = (x + x^{-1})/2 - 1$ is the recognition cost.
background
The recognition cost is $J(x) = (x + x^{-1})/2 - 1$ (also written $\cosh(\log x) - 1$). It is the unique continuous solution of the Recognition Composition Law (RCL) under the usual regularity hypotheses (forcing chain T5). In RS-native units it measures mismatch of positive ratios.
This module runs Campaign 2 Track A: the reparametrization attack on the constraint sector. The paper QG_Constraint_Sector_Recognition_Premise printed a falsifier it had not executed: exhibit a weight clause that is not SatisfiesCompositionLaw, still forces unit weight, and leaves the rest of the model class alone. Section 8 of the HKT kinetic derivation had claimed field-independence of the kinetic weight from RCL alone; the attack tests whether that forcing is RCL-specific or an artifact of a weaker one-point condition.
The predicate here is exactly that weaker condition: agreement of weighted and bare cost at the single sample point $x = 2$, with no composition-law content.
proof idea
Definitional abbreviation only. The body is the equality $w \cdot J(2) = J(2)$; there is no tactic proof and no lemma application. Downstream theorems discharge consequences by rewriting with the numerical identity $J(2) = 1/4$ and applying linear arithmetic.
why it matters
This predicate is the concrete witness that meets the paper's printed falsifier. Downstream, calibratedWeightAtTwo_forces_one shows it forces $w = 1$ more sharply than RCL (which still admits the $w = 0$ branch); not_calibratedWeightAtTwo_zero records that zero fails the clause; calibratedWeightAtTwo_ne_rclWeight proves the predicate is not definitionally the composition-law weight clause; and falsifier_as_printed_is_met packages the two facts into the paper's stated attack condition.
In framework terms the finding is about the gate, not about T5 or RCL themselves: unit weight can be forced by a one-point normalization with no recognition content. The module notes the attack lands at lower severity than the O5 ladder attack, because here the conclusion is a scalar rather than identification of $J$. The declaration therefore closes the printed falsifier while leaving the genuine RCL-based kinetic derivation intact as a stronger, law-level statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.