feat: globalize smoothness of group homomorphisms

[utensil]

This PR globalizes C^n regularity of a group homomorphism from the identity to every source point for the LieGroups Layer 2 automatic-smoothness path.

Roadmap: RepresentationTheory

Summary

Add TauCeti.contMDiff_of_contMDiffAt_one: for any bundled morphism satisfying MonoidHomClass, from a group manifold to a smoothly multiplicative MulOneClass manifold, smoothness at the identity implies smoothness everywhere. Left translation moves the identity germ to an arbitrary point and the homomorphism law identifies the translated expression with the original map. to_additive supplies the zero-based additive analogue. The theorem documentation credits Mathlib's structurally analogous continuous_of_continuousAt_one.

This is the local-to-global boundary used after a closed-graph argument establishes smoothness at the identity. The statement keeps arbitrary differentiability order, field, and source/target models; it assumes neither finite dimensionality nor smooth inversion. No Mathlib source is vendored. The API uses Mathlib's ContMDiffAt.comp_of_eq, MonoidHomClass, and smooth multiplication, at the same structural generality as the adjacent continuous theorem continuous_of_continuousAt_one.

Roadmap target

This advances RepresentationTheory/LieGroups/README.md, Layer 2, “the closed-subgroup (Cartan) theorem,” specifically Cartan's automatic-smoothness corollary for continuous homomorphisms. Its downstream consumer is RepresentationTheory/SpinRepresentations/README.md, Layer 3, “the differential of the double cover”: the abstract Spin and special-orthogonal group homomorphism must become smooth before lieMap can identify its differential. After this PR, the LieGroups milestone still needs the product chart and subgroup atlas, the embedded subgroup structure and graph-local smoothness argument, and the concrete Spin/SO Lie structures.

Verification

• Exact head: f80c298a33b350b5270a56c125056b88935e9771
• Local Lean build: spinrep-validate run -- lake build — passed (11176 jobs)
• Axiom audit: spinrep-validate run -- lake exe axioms — passed (111943 TauCeti declarations; only propext, Classical.choice, and Quot.sound)
• Lint: aggregate git diff --check — passed
• Public CI: passed on the prior published head; pending for this repair head

Scale and generality

The aggregate changes one existing file by 37 added lines and one module-docstring line replacement. It adds one multiplicative theorem and its generated additive counterpart, for arbitrary n : ℕ∞ω, a common nontrivially normed field, unrelated source and target models, a group source, a MulOneClass target, and any bundled morphism implementing MonoidHomClass. The proof uses only smooth multiplication; the inverse is a fixed source element.

Scope

• Consumes: ContMDiffAt.comp_of_eq, smooth pointwise multiplication, MonoidHomClass.map_mul, and group cancellation
• Provides: contMDiff_of_contMDiffAt_one and its to_additive zero-based counterpart
• Fits: isolates the final translation step in automatic smoothness, which supplies smooth homomorphisms to lieMap and ultimately the Spin/SO double-cover differential
• Boundary: no subgroup chart, embedded-manifold structure, closed-graph theorem, automatic-smoothness endpoint, concrete Spin/SO Lie structure, or differential is asserted

_{🤖 GPT-5.6 Sol high · TauCetiWorker @ 7518d4150b846c4524423341570c031027a1d92c · rubrics @ afb424eda89e8ac96d9eb69f6a88972055a4cd1b · local review @ b533e561b6d44df071c31335ed4a63ae647507d2 · fixed: attribution, generality, reuse}

[CBirkbeck]

✅ reuse — now passing on a779dba.

[CBirkbeck]

🟡 attribution — request_changes codex/gpt-5.6-sol

The central Mathlib analogue named in the PR description is not credited in the code.

• TauCeti/Geometry/Manifold/Algebra/Monoid.lean:108 — The theorem docstring omits credit for Mathlib's directly analogous continuous_of_continuousAt_one, which the PR description identifies as its structural model. Fix: Add a docstring reference to continuous_of_continuousAt_one as the continuous analogue motivating this construction.

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 · 25s · 82.2k in / 867 out tokens · reviewing this diff · rubric}

[CBirkbeck]

✅ generality — now passing on a779dba.

[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 theorem and generated additive analogue faithfully globalize regularity using smooth left translation and the homomorphism law; no semantic defect or hidden prerequisite was found.
✅	reuse	approved	codex/gpt-5.6-sol	The declarations are genuinely new: searches across Mathlib and TauCeti found no existing local-to-global ContMDiff theorem, and the proof appropriately reuses Mathlib’s translation, composition, multiplication, and homomorphism APIs.
✅	scope	approved	codex/gpt-5.6-sol	The theorem is a focused, proximate prerequisite for Layer 2’s automatic-smoothness corollary: it converts identity-local smoothness from the graph argument into global smoothness. The PR is a single coherent topic, and the prerequisite Layer 0 infrastructure exists on the PR base.
✅	attribution	approved	codex/gpt-5.6-sol	The code documentation explicitly credits Mathlib's structurally analogous continuous_of_continuousAt_one; no other central formal or informal source is evident.
✅	api-design	approved	codex/gpt-5.6-sol	The public surface is appropriately general and minimal: it exports the required multiplicative theorem and additive counterpart without exposing implementation details or compatibility artifacts.
✅	generality	approved	codex/gpt-5.6-sol	The theorem is stated at the natural generality: arbitrary differentiability order and MonoidHomClass morphisms, with exactly the source and target multiplication regularity used by the translation proof.
✅	placement	approved	codex/gpt-5.6-sol	The theorem is canonically placed with the existing smooth monoid-morphism API, and the sole Mathlib import directly supplies the manifold monoid machinery it uses.
✅	naming	approved	codex/gpt-5.6-sol	The theorem name follows Mathlib’s conclusion-outward convention and matches the adjacent continuous_of_continuousAt_one precedent; the generated additive name and TauCeti namespace are appropriate.
✅	documentation	approved	codex/gpt-5.6-sol	The module docstring and both theorem docstrings accurately describe the added local-to-global smoothness result, its additive analogue, and the absence of a smooth-inversion requirement.
✅	proof-quality	approved	codex/gpt-5.6-sol	The proof is short and robust; its sole change is locally documented and only exposes function composition for comp_of_eq, while the remaining steps use stable structural lemmas and straightforward algebraic simplification.

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

_{Reviewing this diff at head f80c298. rubrics @ afb424e. Review spend: $1.89.}