rHatEmergenceCert
plain-language theorem explainer
The definition supplies a concrete certificate that the recognition operator emerges uniquely as the J-cost decreasing map with fixed point at unity. Pre-Big-Bang dynamics researchers cite it to ground the structural claim of paper §6. The construction is a direct record that populates the three required fields from prior fixed-point and Lyapunov lemmas.
Claim. Let $J(x) = (x-1)^2/(2x)$ denote the J-cost. The midpoint map $m(x) = (x+1)/2$ satisfies $m(1)=1$ and $J(m(x)) < J(x)$ for all $x>0$, $x≠1$. Any map $f$ obeying the same fixed-point and strict decrease conditions has unique fixed point at 1. This supplies the emergence certificate for the recognition operator.
background
The module formalizes the pre-Big-Bang §6 claim that the recognition operator emerges from gradient descent on the J-cost landscape. J-cost is the function $J(x) = (x-1)^2/(2x)$ that vanishes at $x=1$ and serves as a strict Lyapunov function. The midpoint map is the linear contraction $x ↦ (x+1)/2$ whose fixed point is exactly 1. The RHatEmergenceCert structure packages three facts: the midpoint map fixes 1, decreases J-cost away from 1, and any other map obeying the same two properties must also fix only at 1.
proof idea
The definition is a one-line wrapper that supplies the three fields of the RHatEmergenceCert structure. It assigns the fixed-point theorem for the midpoint map to the first field, the J-cost decrease theorem for the midpoint map to the second field, and the uniqueness theorem for any J-cost decreasing map to the third field.
why it matters
This declaration converts the SCAFFOLD annotation in pre-Big-Bang paper §6 into structural theorem status by exhibiting the unique J-cost Lyapunov map. It directly implements the gradient-flow uniqueness statement of the module doc-comment. No downstream results depend on it yet, leaving open the question of how the certificate lifts to the full recognition operator in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.