geodesicOneSimplex_self

This module lifts path-level winding and displacement on the circle to singular simplices of $S^1$, and proves that displacement vanishes on boundaries of $2$-simplices. That identity, with the once-around generator mapping to winding $1$, supplies the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.

A geodesic $1$-simplex is the projection of the straight-line path in the universal cover $\mathbb{R}\to S^1$ between two real lifts $a$ and $b$: on a point $x$ of the standard $1$-simplex it evaluates the trigonometric circle map at the convex combination $(1-x_1)a+x_1 b$. The constant $1$-simplex at a point $p\in S^1$ is the continuous map sending every simplex point to $p$. The trigonometric circle point of a real parameter is the standard once-around embedding of that angle into the exact $S^1$ object.

Pointwise equality of continuous maps on the standard $1$-simplex. After ext, the evaluation lemma for geodesics reduces the left-hand side to the trigonometric point of $(1-x_1)a+x_1 a$. A one-line ring identity collapses that combination to $a$, and definitional equality with the constant simplex finishes the proof.

Degenerate geodesics must be identified with constant edges before they can bound constant $2$-simplices in free singular chains. Downstream, geodesicFreeChain_self_bounds rewrites a self-geodesic free chain through this identity and the constant-simplex comparison, proving a degenerate geodesic bounds a constant $2$-simplex. The same collapse appears in the terminal-side correction for oriented cyclic families: cyclic connectivity forces consecutive lift endpoints to agree modulo $2\pi\mathbb{Z}$, so terminal-return geodesics become (shifted) self-geodesics and may be replaced by constants when assembling the bounding $2$-chain. That correction is part of the generation half of the winding comparison on $1$-cycles, complementing the module's kills-boundaries identity toward $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.