RHatEmergenceCert
plain-language theorem explainer
R̂ emerges as the unique J-decreasing map with fixed point at 1. Pre-Big-Bang modelers cite this structure to certify that gradient flow on the J-cost landscape forces any admissible update rule to contract toward unity. The definition packages three properties: fixed point of the midpoint map at 1, strict J-cost decrease under that map, and uniqueness of the fixed point at 1 for every J-cost Lyapunov map.
Claim. Let $J$ be the J-cost function and let $m(x) = (x + 1)/2$ be the midpoint map. A certificate consists of the three statements $m(1) = 1$, $J(m(x)) < J(x)$ for all $x > 0$ with $x ≠ 1$, and the uniqueness property that any map $f : ℝ → ℝ$ satisfying $f(1) = 1$ and $J(f(x)) < J(x)$ for $x > 0$, $x ≠ 1$ has no positive fixed point other than 1.
background
The module formalizes the emergence of the recognition operator R̂ as the unique gradient-descent dynamics on the J-cost landscape, following the pre-Big-Bang §6 scaffold. J-cost functions as a strict Lyapunov function for the midpoint map, which is the explicit linear contraction $x ↦ (x + 1)/2$ supplied by the upstream definition midpointMap. The local theoretical setting is the claim that any smooth positive-real update rule that decreases J-cost at every step and fixes exactly at unity must be a contraction toward 1, with the unique linear case being the recognition operator.
proof idea
The declaration is a structure definition that directly records three independent properties without further proof steps. The first field asserts the fixed point of midpointMap at 1, the second asserts strict J-cost decrease under midpointMap, and the third asserts uniqueness of the fixed point at 1 for any map obeying the same Lyapunov condition. No tactics are used; the structure simply aggregates the three facts for later instantiation.
why it matters
This supplies the structural certificate that converts the SCAFFOLD annotation in pre-Big-Bang §6 into theorem status by encoding uniqueness of R̂ as the J-cost gradient flow. It feeds directly into the downstream definition rHatEmergenceCert, which instantiates the three fields using midpointMap properties. In the Recognition Science framework the result anchors pre-Big-Bang dynamics to J-uniqueness (T5) and the forced self-similar fixed point (T6), establishing that the recognition operator is the only admissible update rule before the Big Bang.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.