lawful_normalizer_exists_unique
plain-language theorem explainer
The lemma proves existence and uniqueness of a real number satisfying the LawfulNormalizer predicate, which requires equality to 1 together with the EL stationarity and global minimality properties. Workers on the URC adapter layer cite this result to anchor the lambda-recursion uniqueness at the trivial fixed point under abstract obligations. The proof is a direct term-mode application of ExistsUnique.intro that supplies the constant 1 for existence via the EL_holds lemma and extracts the fixed-point equality for uniqueness.
Claim. There exists a unique real number $x$ such that $x=1$ and the EL stationarity and global minimality conditions hold.
background
In the URCAdapters module the LawfulNormalizer structure on a real parameter $x$ is defined to require both a fixed-point condition $x=1$ and satisfaction of the EL_prop predicate. The EL_prop predicate is witnessed by the upstream EL_holds lemma, which packages Cost.EL_stationary_at_zero together with Cost.EL_global_min. The target declaration supplies a Prop-level witness for the sibling definition lambda_rec_unique, which asserts ExistsUnique (fun x : ℝ => LawfulNormalizer x).
proof idea
The proof is a term-mode construction that applies ExistsUnique.intro to the concrete value 1. Existence is discharged by an exact pairing of reflexivity with the EL_holds lemma. Uniqueness follows from a direct intro-exact sequence that extracts the fixed field of any LawfulNormalizer hypothesis.
why it matters
This lemma completes the lambda_rec_unique proposition inside the URCAdapters layer, furnishing the base case for the normalizer at unity under the current abstract obligations. It fills the prop-level witness role described in the module documentation for the lambda-rec bridge, which will be refined once the ethics alignment hook is exposed. No downstream uses are recorded, indicating it serves as foundational scaffolding for further URC developments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.