feat: base-point change for higher homotopy groups

[sqrt-of-2]

This PR proves that a path from x to y induces a group isomorphism between the higher homotopy groups based at the two points, TauCeti.homotopyGroupMulEquivOfPath : HomotopyGroup N X x ≃* HomotopyGroup N X y for a finite nonempty index type N, together with its functoriality in the path. This is the last unmet item of Stage 3, milestone 9 of TauCetiRoadmap/UniversalCovers/README.md, whose π_n API asks for "functoriality, pointed maps, the boundary-relative homotopy API on Ω^N, (pre)connectedness of cubes and cube boundaries for n ≥ 2, and basepoint-change isomorphisms"; every other part of that list is already in the repository, and after this PR Stage 3 is complete, leaving the roadmap's open work in the Galois-category lens of Stage 2 item 8 and in the remaining Stage 4 examples.

The construction is the classical collar argument, organised so that one canonicity lemma does all the later work. TauCeti.cubeRad, defined as twice the distance to the centre of the cube, is continuous because the product metric on I^N is the sup metric for finite N, and it equals 1 exactly on Cube.boundary N; TauCeti.cubeScale rescales radially and multiplies the radius. TauCeti.collar glues an inner family of cube maps, rescaled onto the full cube, to an outer family of paths reparametrised along the collar, the two branches agreeing where the rescaling lands on the cube boundary. With the shrinking radius (2 - t)/2 this is TauCeti.GenLoop.collarHomotopy, and TauCeti.GenLoop.transport γ f is defined as its value at time 1.

TauCeti.GenLoop.HomotopyAlong γ f g records a homotopy from f to g restricting to γ on the cube boundary, and TauCeti.GenLoop.HomotopyAlong.homotopic_transport says every such homotopy ends at a loop homotopic, relative to the boundary, to transport γ f. This is the homotopy extension property of the pair (I^N, Cube.boundary N) in the only form needed, and it is proved concretely: an explicit radial retraction TauCeti.cubeRetract sends the top face of the cylinder I × I^N onto its bottom face together with its sides, composing a homotopy along γ with it reproduces transport γ f on the nose, and the straight-line homotopy in the convex cylinder from the identity to that retraction is stationary on the boundary. Consequently the concatenation law, the constant-path law and multiplicativity each reduce to exhibiting one homotopy along the relevant path — two collar homotopies concatenated in the time direction, the constant homotopy, and two collar homotopies concatenated in a cube direction. That transport respects homotopy of generalized loops, and depends only on the homotopy class of the path, is instead read off from the collar of a continuous family, TauCeti.transportFamily. The group structure enters only through Mathlib's HomotopyGroup.mul_spec.

The mathematics is standard (Hatcher, Algebraic Topology, Section 4.1), and no Mathlib source was vendored: Mathlib's Ω^ N X x, HomotopyGroup, Cube.boundary, ContinuousMap.HomotopyRel, Path.Homotopic.trans_symm/symm_trans and Set.projIcc are consumed as they stand, and the result is the higher-dimensional analogue of Mathlib's existing FundamentalGroup.fundamentalGroupMulEquivOfPath. The new cube geometry needed a home beside the existing cube file, so that file becomes a directory in the same PR; the module table is

old module	new module
TauCeti.Topology.Homotopy.Cube	TauCeti.Topology.Homotopy.Cube.Basic

with no declaration renamed, and the single importer, TauCeti.Topology.Homotopy.HomotopyGroup.Covering, updated.

Roadmap: UniversalCovers

🤖 Prepared with Claude Code

[sqrt-of-2]

⛔ reuse — block codex/gpt-5.6-sol

Two new endpoint lemmas directly duplicate existing Set.projIcc API and should be removed.

• TauCeti/Topology/Homotopy/Cube/Radius.lean:62 — projIcc_zero and projIcc_one are specialization-only wrappers directly replaced by Set.projIcc_left and Set.projIcc_right. Fix: Delete both declarations and use Set.projIcc_left/Set.projIcc_right directly at all call sites, with rfl or norm_num where subtype endpoint normalization is needed.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 29s · 155.4k in / 797 out tokens · reviewing this diff · rubric}

[sqrt-of-2]

AI review — blocked

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	codex/gpt-5.6-sol	The new transport construction, canonicity theorem, functoriality laws, and induced multiplicative equivalence faithfully formalize base-point change for nonzero-dimensional homotopy groups. No semantic defect or vacuous prerequisite was found.
⛔	reuse	blocked	codex/gpt-5.6-sol	Two new endpoint lemmas directly duplicate existing Set.projIcc API and should be removed.
▫️	scope	not yet run	—
▫️	attribution	not yet run	—
▫️	api-design	not yet run	—
▫️	generality	not yet run	—
▫️	placement	not yet run	—
▫️	naming	not yet run	—
▫️	documentation	not yet run	—
▫️	proof-quality	not yet run	—

♻️ = approved on an earlier commit, re-run before merge. Halted at the reuse block; the deferred rubrics run once it clears.

_{Reviewing this diff at head 85b0f46. rubrics @ f854a7e. Review spend: $0.46.}

[kbuzzard]

🟡 api-design — request_changes codex/gpt-5.6-sol

The general higher-homotopy equivalence unnecessarily exposes a decidable-equality requirement, and two canonical reduction lemmas are missing simp annotations.

• TauCeti/Topology/Homotopy/HomotopyGroup/BasepointChange.lean:354 — homotopyGroupMulEquivOfPath and every general theorem built from it require [DecidableEq N], although the advertised construction only needs finite nonempty N; this leaks a proof implementation choice into the canonical API. Fix: Remove [DecidableEq N] from homotopyGroupMulEquivOfPath, its _mk, _apply, _symm_apply, _refl, _trans, _congr, _symm lemmas, and nonempty_homotopyGroupMulEquiv; install Classical.decEq N locally for the transAt proof.
• TauCeti/Topology/Homotopy/HomotopyGroup/BasepointChange.lean:321 — Canonical normalization lemmas are inconsistently annotated: homotopyGroupTransport_trans and homotopyGroupMulEquivOfPath_symm_apply lack @[simp], despite reducing concatenation and inverse application to the established transport normal form. Fix: Add @[simp] to both lemmas; their orientations reduce compound operations and do not introduce a rewrite loop.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 34s · 71.7k in / 1.6k out tokens · reviewing this diff · rubric}

[sqrt-of-2]

I implemented the valid part of this finding on 4543b98: homotopyGroupTransport_trans is now @[simp], and the full linter-enabled lake build passes. The other two requests are not valid against this Mathlib pin. First, Mathlib defines HomotopyGroup.group (N) [DecidableEq N] [Nonempty N] : Group (HomotopyGroup N X x) and HomotopyGroup.mul_spec under the same [DecidableEq N] section; removing the assumption makes the exported MulEquiv result itself fail to synthesize Mul (HomotopyGroup N X x). Installing Classical.decEq locally changes the typeclass identity and does not definitionally agree with canonical instances (for example Fin.instDecidableEq). This exact evidence already cleared the corresponding generality finding in reply 3839828331 / re-review 3840016705. Second, homotopyGroupMulEquivOfPath_symm_apply must not be tagged @[simp]: commit 3b44af8 removed that attribute because the simpNF linter reports the lemma is already normalized by the existing simp lemmas homotopyGroupMulEquivOfPath_symm and homotopyGroupMulEquivOfPath_apply. Re-adding it would violate the repository requirement not to silence linters. Current verification after retaining both constraints: lake build completed successfully (9072 jobs), and lake exe axioms audited 71008 declarations with all axioms in the allowlist.

[CBirkbeck]

Re: your reply on api-design — re-reviewed on 4543b98; the finding stands — The main basepoint-change API is present, but it exposes proof-only collar machinery and omits a normal-form simp annotation for inverse application.

_{codex/gpt-5.6-sol · addresses your replies through comment 3840087519.}

[kbuzzard]

AI review — changes requested

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
♻️	correctness	stale (re-run pending)	codex/gpt-5.6-sol	The collar construction, radial retraction, induced transport, and group-isomorphism statements faithfully formalize base-point change; no semantic defect was found.
♻️	reuse	stale (re-run pending)	codex/gpt-5.6-sol	No material reuse or duplication issue is established by the supplied diff; the new specializations have genuine consumers and the higher-homotopy basepoint-change API is distinct from Mathlib's fundamental-group result.
♻️	scope	stale (re-run pending)	codex/gpt-5.6-sol	The PR directly implements the cited Stage 3 item 9 basepoint-change isomorphism, and its cube-radius, collar, transport, and module-relocation changes form one coherent topic.
♻️	attribution	stale (re-run pending)	codex/gpt-5.6-sol	The code credits the central informal source (Hatcher, Section 4.1), the roadmap item, and the analogous Mathlib construction; no vendored or closely adapted uncredited formal source is evident.
🟡	api-design	changes requested	codex/gpt-5.6-sol	The general higher-homotopy equivalence unnecessarily exposes a decidable-equality requirement, and two canonical reduction lemmas are missing simp annotations.
✅	generality	approved	codex/gpt-5.6-sol	The assumptions match Mathlib’s current homotopy-group API: its group structure and multiplication theorem require [DecidableEq N], so the contested constraint is not removable without changing typeclass identity. No material generality issue remains.
♻️	placement	stale (re-run pending)	codex/gpt-5.6-sol	The new cube geometry and basepoint-change declarations are placed in canonical topic subdirectories, the Cube module relocation is complete, and the imports match the evident dependencies.
♻️	naming	stale (re-run pending)	codex/gpt-5.6-sol	The introduced names accurately describe their conclusions in standard Mathlib terminology, follow adjacent base-point-change conventions, and introduce no new notation.
✅	documentation	approved	codex/gpt-5.6-sol	The new substantive modules and their public API are documented accurately; the previously undocumented transport functoriality theorems now have declaration-level docstrings.
✅	proof-quality	approved	codex/gpt-5.6-sol	The current proofs are robust and readable; the only change exposing definitional equality is locally documented and justified by Mathlib’s quotient-wrapper API.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 3b44af8. rubrics @ f854a7e. Review spend: $2.49.}

[CBirkbeck]

✅ reuse — now passing on 85fc4af.

[CBirkbeck]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	codex/gpt-5.6-sol	The radial collar construction, canonicity retraction, transport laws, and multiplicative equivalence faithfully establish base-point change for finite nonempty higher homotopy groups.
✅	reuse	approved	codex/gpt-5.6-sol	The cube-radius, collar transport, and higher-homotopy basepoint-change APIs are not duplicated in Mathlib or TauCeti, and the implementation reuses the relevant existing homotopy, cube, projection, convex-combination, and homotopy-group operations.
✅	scope	approved	codex/gpt-5.6-sol	The PR directly implements the basepoint-change isomorphisms required by UniversalCovers Stage 3, item 9. The radial cube geometry, collar transport, functoriality results, and cube-module relocation form one coherent unit.
✅	attribution	approved	codex/gpt-5.6-sol	The central collar construction credits Hatcher, Section 4.1, and the code identifies the analogous Mathlib base-point-change declaration and HomotopyGroup.mul_spec; no uncredited adapted source is evident.
✅	api-design	approved	codex/gpt-5.6-sol	The canonical basepoint-change interface is complete and appropriately annotated; proof-specific family and retraction machinery remains private, with no obsolete compatibility surface.
✅	generality	approved	codex/gpt-5.6-sol	The declarations are at the natural level: cube geometry requires finiteness, while the multiplicative API’s Nonempty N and DecidableEq N assumptions are required by Mathlib’s group instance.
✅	placement	approved	codex/gpt-5.6-sol	The new declarations are placed in coherent Cube and HomotopyGroup submodules, the old flat Cube module is removed with its importer updated, and the current imports are appropriately scoped.
✅	naming	approved	codex/gpt-5.6-sol	Introduced names accurately describe their conclusions using standard homotopy and cube-geometry terminology, follow the existing fundamental-group precedent, and introduce no notation.
✅	documentation	approved	codex/gpt-5.6-sol	The new substantive modules and public API are documented accurately, and the retraction description correctly distinguishes the cylinder projection from its top-face restriction.
✅	proof-quality	approved	codex/gpt-5.6-sol	The proofs are robust and readable. The sole change is locally documented and justified by Mathlib’s missing quotient-wrapper API, while explicit evaluation lemmas avoid undocumented definitional-equality manipulation elsewhere.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 85fc4af. rubrics @ f854a7e. Review spend: $9.22.}

[CBirkbeck]

✅ api-design — now passing on 85fc4af.

[sqrt-of-2]

Fixed on e17fd44, with one adjustment on the third item.

1. transportFamily, transportFamily_apply, transportFamily_apply_eq_transport and transportFamily_apply_of_mem_boundary are now private.
2. cubeTopFaceRetract (renamed from cubeRetract for the naming finding), cubeTopFaceRetract_apply, cubeTopFaceRetract_of_mem_boundary and HomotopyAlong.map_cubeTopFaceRetract are now private, leaving HomotopyAlong.homotopic_transport as the public result. It is also dropped from the ## Main declarations list.
3. homotopyGroupMulEquivOfPath_symm_apply now carries @[simp]. Adding the attribute while homotopyGroupMulEquivOfPath_symm also had it is not possible: simpNF rejects it, because the composite of the two existing simp lemmas already normalises the left-hand side. Verbatim output of #lint only ... simpNF ... in TauCeti.Topology.Homotopy on that intermediate state:

-- TauCeti.Topology.Homotopy.HomotopyGroup.BasepointChange
#check @TauCeti.homotopyGroupMulEquivOfPath_symm_apply /- simp can prove this:
  by simp only [*, @TauCeti.homotopyGroupMulEquivOfPath_symm, @TauCeti.homotopyGroupMulEquivOfPath_apply]
One of the lemmas above could be a duplicate.
If that.s not the case try reordering lemmas or adding @[priority]. -/

Since silencing a linter is not allowed in this repository, I made homotopyGroupMulEquivOfPath_symm_apply the simp-normal form as requested and dropped @[simp] from homotopyGroupMulEquivOfPath_symm instead. The simp normal form of (homotopyGroupMulEquivOfPath γ).symm a is unchanged — it was, and still is, homotopyGroupTransport γ.symm a, now reached in one rewrite rather than two — and homotopyGroupMulEquivOfPath_symm is retained as a plain lemma. With that arrangement the same #lint run reports 0 errors in 70 declarations ... All linting checks passed!.

Verification of the whole commit: lake build completed successfully (9072 jobs); lake exe axioms audited 71011 declarations, all within [propext, Classical.choice, Quot.sound].

[CBirkbeck]

Re: your reply on api-design — re-reviewed on e17fd44; this clears the finding ✅ — approved on e17fd44.

_{codex/gpt-5.6-sol · addresses your replies through comment 3840317234.}

[CBirkbeck]

✅ naming — now passing on 85fc4af.

[CBirkbeck]

✅ documentation — now passing on 85fc4af.

[CBirkbeck]

✅ proof-quality — now passing on 85fc4af.

[sqrt-of-2]

Fixed on e17fd44 by adding the explicit evaluation lemmas, as the first branch of the suggested fix. All four flagged change steps are gone.

• HomotopyAlong.map_boundary is now stated through the coercion of the underlying homotopy (toHomotopy (t, z) = γ t) instead of the inherited raw toFun field. That is what forced the change at line 174: with the new spelling the goal in HomotopyAlong.trans is already ⇑(h₁.toHomotopy.trans h₂.toHomotopy) (t, z) = (γ.trans δ) t, so ContinuousMap.Homotopy.trans_apply rewrites directly. The unusedTactic linter confirms the step had become a no-op ("change ... does nothing") before I deleted it.
• The homotopy underlying HomotopyAlong.transAt is split off as a private transAtHomotopy, with a private evaluation lemma transAtHomotopy_apply. Its map_boundary field is then proved by rw [transAtHomotopy_apply], no change.
• The remaining two goals were map_zero_left/map_one_left, whose right-hand sides are values of Mathlib’s GenLoop.transAt, which has no evaluation lemma upstream. A private transAt_apply supplies one (it is rfl, since GenLoop.transAt is a GenLoop.copy of exactly that half-and-half split), and the two proofs are now dsimp only; rw [GenLoop.coe_copy-style lemma GenLoop.coe_coe, transAt_apply]; split_ifs. Both new declarations are private, matching the api-design finding on this PR that proof-only machinery should not be exposed.

The one change still in the file is the pre-existing one in homotopyGroupMulEquivOfPath.map_mul, which carries the three-line comment explaining that Mathlib’s HomotopyGroup.mul_spec has an open TODO for a HomotopyGroup.mk API and that the wrapper must be exposed for mul_spec to rewrite; this rubric approved that step explicitly on 3b44af8 ("the only change exposing definitional equality is locally documented and justified by Mathlib’s quotient-wrapper API").

Verification: lake build completed successfully (9072 jobs); lake exe axioms audited 71011 declarations, all within [propext, Classical.choice, Quot.sound]; the #lint environment-linter set over TauCeti.Topology.Homotopy reports "All linting checks passed!".

[CBirkbeck]

Re: your reply on proof-quality — re-reviewed on e17fd44; this clears the finding ✅ — approved on e17fd44.

_{codex/gpt-5.6-sol · addresses your replies through comment 3840318263.}

[CBirkbeck]

✅ placement — now passing on 85fc4af.