Create Lean projects atomically

[Deicyde]

Depends on #85 and is based directly on its upstream branch.

Summary

• add autoform project new for an absent target and an explicit bundled
  Lean/Mathlib release
• generate the Lean shell, Autoform blueprint, docs config, complete exact
  nine-package Lake lock, and optional verified workflows without running
  project code during planning
• serialize cooperative creators, stage on the destination filesystem, verify
  exact bytes/types/modes/ownership/links through retained descriptors, and
  publish with a native atomic no-replace rename
• preserve failed stages and report prepublish failure, committed success, or
  commit-uncertain state accurately

Review hardening

• keep public catalog/inspection v1 unchanged; use a private per-release
  creation descriptor that cross-checks public release identity, complete Lake
  manifest, and all reserved dependency roots (including Archive,
  Counterexamples, and MathlibTest)
• reject package names that collide with dependency/toolchain roots and reject
  overlong or surrogate paths before staging
• bind the requested parent by no-follow dev/inode/uid immediately before
  publication and again after parent fsync; preserve the stage on prepublish
  drift and report exact published/synced state on postpublish drift
• require safe sticky-directory ownership and verify staged ownership/link count
• exercise the real no-replace syscall with a late existing destination rather
  than mocking the primitive
• keep postcommit human and JSON output ASCII/backslash-safe, including under
  PYTHONIOENCODING=ascii

This is a clean reconstruction of the project-creation feature delta on #85,
without the stale merge history or removed #14 private APIs from old #26.

Validation

• Python 3.10 create/inspect/provenance/scaffold/wheel gate: 591 passed, 1 skipped
• Python 3.13 equivalent: 591 passed, 1 skipped
• post-bundle focused gates: 297 create/inspect/wheel; 92 scaffold/skills;
  108 full create; 35 final root/skill tests
• 59 independent adversarial selections: passed
• full Ruff, git diff --check, and make check-example: passed
• real Lake accepted the generated complete manifest, checked out every exact
  dependency, and began compilation; local cache extraction then hit shared
  ENOSPC, so fresh CI owns the complete-build proof
• real-Lean CI now creates a project, runs cache retrieval and lake build
  under explicit step bounds with a 75-minute job ceiling

Independent review found no remaining correctness blocker.

[Deicyde]

Python 3.10/3.13 and Windows gates are green. Both real-Lean jobs failed only in the unchanged #65 detached-child PID-file fixture before reaching the generated-project build. #67 now fixes that test and its full Python/Windows/real-Lean CI is green, but it remains blocked on contributor CLA. Keeping this stack awaiting that dependency rather than weakening or retrying the flaky gate.

[Deicyde]

Restacked additively onto final #85 head 22a8ba5; current head is 2e5a86d. Post-restack create/inspection/provenance/scaffold/wheel/skill gate: 649 passed, 1 skipped; Ruff, diff check, and make check-example pass. Project-creation behavior is unchanged.

[Deicyde]

Superseded by #96, which rebuilds project creation on main without the provenance dependency and loosens the single-release lock.