one
plain-language theorem explainer
Definition of the unit element in the integers obtained as the Grothendieck completion of the naturals forced by logic. Action-functional proofs cite it when normalizing paths to the cost minimum and when proving rigidity of solutions to the cost-rate equation. The construction is a direct application of the pair constructor to the successor of the identity element paired with the identity element.
Claim. Let $Z_ℓ$ be the Grothendieck completion of the naturals $N_ℓ$ forced by logic. The unit element is the equivalence class of the pair consisting of the successor of the identity element of $N_ℓ$ and the identity element itself.
background
In the foundation layer, natural numbers arise as the smallest set closed under a generator starting from the zero-cost identity element. This structure mirrors the multiplicative orbit {1, γ, γ², ...} inside the positive reals. The integers are then obtained by the Grothendieck construction: pairs of naturals modulo the relation (a, b) ~ (c, d) precisely when a + d = b + c.
proof idea
One-line wrapper that applies the pair constructor to the successor of the identity natural and the identity natural.
why it matters
This unit anchors normalization in the cost-rate Euler-Lagrange analysis, where the only positive solutions are the constant path at value one. It supports the convexity proofs for the J-action functional and the uniqueness of action minimizers. It feeds the rigidity result that admissible paths satisfying the cost-rate equation are constantly one, and the global minimum theorems for the action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.