one
plain-language theorem explainer
The multiplicative identity 1 lies in the subfield of the reals generated by any real parameter φ. Researchers deriving admissible paths for the J-cost action and checking algebraic closure in the recognition specification cite this to confirm the constant path at the J-minimum is always available. The proof is a one-line term that invokes the unit membership property of the generated subfield.
Claim. For every real number $φ$, the number $1$ belongs to the subfield of $ℝ$ generated by $φ$.
background
The RecogSpec.Core module introduces phiSubfield φ as the smallest subfield of the reals containing the set {φ}. PhiClosed φ x is the predicate asserting that x lies in this subfield, so x is obtained from φ by the field operations together with rational coefficients. This algebraic restriction on admissible values supports the specification of paths whose costs remain inside the structure fixed by the forcing chain.
proof idea
The proof is a one-line term that applies the one_mem property of the subfield generated by φ.
why it matters
This membership feeds directly into downstream results on the rigidity of Euler-Lagrange critical points for the cost-rate action and into the convexity and uniqueness theorems for the J-action functional. It supplies the base algebraic fact that the constant path at value 1 satisfies the closure condition required by the recognition specification, thereby anchoring the global minimum of J. The result touches the T5 uniqueness step for the J-map without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.