hequivProdContractible
plain-language theorem explainer
Product with a contractible space is homotopy equivalent to the original factor. Topologists working the punctured-sphere covers of $S^{n+1}$ cite this to drop the radial (or other contractible) factor after polar coordinates. The construction multiplies the identity homotopy equivalence by the contractible-to-unit equivalence, then applies $Z\times\mathrm{Unit}\simeq Z$.
Claim. Let $Z$ and $C$ be topological spaces, and suppose $C$ is contractible. Then there is a homotopy equivalence $Z \times C \simeq_h Z$.
background
In the singular-sphere geometry module one works with open covers of $S^{n+1}$ obtained by deleting the north and south poles. After stereographic projection and polar coordinates, the relevant pieces appear as products of a lower-dimensional sphere (or punctured sphere) with a contractible radial factor (a ray or an interval).
A space $C$ is contractible when it is homotopy equivalent to a point; Mathlib packages this as ContractibleSpace, which supplies a homotopy equivalence $C \simeq_h \mathrm{Unit}$. The product of homotopy equivalences is again a homotopy equivalence, and $Z \times \mathrm{Unit}$ is canonically homeomorphic to $Z$.
The present definition packages that standard collapse so later sphere-cover arguments can invoke a single named map rather than rebuild the composite each time.
proof idea
One-line composite of three standard maps. Start from the product of the identity homotopy equivalence on $Z$ with a chosen homotopy equivalence $C \simeq_h \mathrm{Unit}$ coming from ContractibleSpace.hequiv_unit. Compose on the right with the homotopy equivalence induced by the canonical homeomorphism $Z \times \mathrm{Unit} \cong Z$ (Homeomorph.prodUnique). The result is a homotopy equivalence $Z \times C \simeq_h Z$.
why it matters
Step 2 of the singular-sphere cover argument needs exactly this collapse: after identifying the intersection of the two punctured covers with a product of $S^n$ and a contractible radial factor, interHomotopyEquiv applies the present map to obtain $S^n$. The same pattern appears in twoPointComplHEquiv, which realizes $S^{n+1}\setminus{p,q}\simeq_h S^n$ by stereographic projection, translation, polar coordinates, and collapse of the ray factor.
Within Recognition Science this is pure supporting topology for the foundation layer (linking and sphere geometry used upstream of dimension and octave arguments). It does not itself force $D=3$ or the eight-tick period; it only clears the homotopy type of the covers those arguments rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.