lambda_rec_unique
plain-language theorem explainer
lambda_rec_unique defines the proposition asserting existence and uniqueness of a real number x satisfying LawfulNormalizer x. Researchers on URC adapters cite it when establishing the trivial normalizer at 1 under abstract stationarity obligations. The definition directly applies the ExistsUnique quantifier to the predicate from the LawfulNormalizer structure.
Claim. There exists a unique real number $x$ such that $x=1$ and the EL property holds.
background
LawfulNormalizer is a structure on a real $x$ that requires the fixed condition $x=1$ together with the EL_prop. This predicate supplies the content for the uniqueness claim inside the URCAdapters layer. The module imports Mathlib and assembles adapters that draw on forcing self-reference structures and mechanism design results to encode stationarity and scaling invariance.
proof idea
The declaration is a direct definition that applies the ExistsUnique constructor from Mathlib to the LawfulNormalizer predicate on reals. No lemmas are applied and no tactics are used beyond the structure definition itself.
why it matters
It supplies the target proposition proved by the sibling lemma lawful_normalizer_exists_unique, which exhibits the witness at 1 using EL stationarity and confirms uniqueness. The definition stands in for the concrete lambda_rec bridge in the URC adapter layer until the ethics alignment hook is added. It aligns with the self-similar fixed point step in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.