LawfulNormalizer
plain-language theorem explainer
LawfulNormalizer defines the property that a real number x qualifies as a lawful normalizer precisely when it equals 1 and the EL_prop predicate holds for the Jlog cost. Researchers on URC adapters cite it when proving uniqueness of the recurrence parameter under abstract stationarity obligations. The declaration is a pure structure definition that bundles the fixed-point field with the imported EL predicate.
Claim. A real number $x$ is a lawful normalizer when $x=1$ and the derivative of the cost function $J_{log}$ vanishes at the origin while $J_{log}(0)$ is its global minimum over all real arguments.
background
In the URCAdapters module the EL_prop predicate encodes first-order stationarity together with global minimality of the logarithmic cost: its definition requires the derivative of Cost.Jlog at zero to vanish and Cost.Jlog(0) to be less than or equal to Cost.Jlog(t) for every real t. LawfulNormalizer packages this predicate with the additional fixed-point requirement that the normalizer parameter itself equals unity. The upstream EL_prop supplies the concrete analytic conditions any candidate normalizer must obey under the current abstract obligations.
proof idea
This is a structure definition with no proof body. It simply declares two fields: fixed, which forces the equality x=1, and EL, which directly imports the EL_prop predicate from the sibling ELProp module.
why it matters
LawfulNormalizer supplies the predicate inside the ExistsUnique statement lambda_rec_unique. The downstream lemma lawful_normalizer_exists_unique constructs the witness at x=1 by supplying the fixed-point equality together with an instance of EL_holds, thereby establishing existence and uniqueness of the normalizer under present obligations. In the Recognition framework this supplies the trivial normalizer that satisfies stationarity and scaling invariance, standing in for the concrete lambda_rec bridge until the ethics alignment hook is exposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.