Formalize: generated import roots serialize independent PR publication #466

Consumer scenario

A Lean repository has deterministic generated library/domain roots, for example
Lib.lean and Lib/Topology.lean, which import the tracked leaf modules.
Several workers contribute disjoint mathematical source files. The project uses
Autoform claims because another session or machine also works on that repository.
One lead coordinates a pool of 12 subagents and publishes independently checked
batches of roughly 1,000–5,000 changed lines.

Problem

The current module claim treats a generated import root as an author-owned Lean
module. Formalize's integration rules retain the complete author/import claim set
until the candidate is integrated and pushed. A worker can therefore keep a root
claim while doing a much longer proof task. Every other batch needing a generated
entry then waits behind that claim, even when its mathematical source is disjoint.
Renewing the lease keeps this publication dependency active indefinitely. Moving
from two primary sessions to one lead with many subagents does not remove the
shared-root dependency when another machine is active.

This puts completed mathematical work into a release queue. Omitting the generated
entries is not a usable workaround: the consumer repository's root-generation check
rejects the PR. Releasing or taking another worker's live author claim is also not a
correct integration protocol.

Observed evidence

In a real claims-enabled run:

• Several independently checked source batches accumulated locally while generated
  roots remained held by another active machine.
• The oldest batch was rebased onto current main: 29 source/test files, 2,791
  insertions and 4 deletions.
• All seven repository preflight checks outside root generation passed.
• Its deterministic generated-root patch contained only 26 import additions and
  zero import deletions. Two of the affected roots had live foreign author claims.
• The lead had to request a manual, generated-import-only exception to publish it.

These are observed workflow facts, not a controlled throughput benchmark. Repeated
large-module compilation and detailed review/capture work also contributed to the
queue; those existing work-package/artifact-reuse problems are tracked separately.

Minimal reproduction

1. Use a fixture repository whose generator derives a domain import root from
   Git-tracked Lib/Domain/*.lean leaves and whose CI checks that root.
2. Worker A acquires a leaf/article plus Lib.Domain as an import-edit author claim
   and keeps renewing that complete set while its proof candidate is unfinished.
3. Worker B completes and verifies a separate leaf under the same domain.
4. B regenerates the expected root: it adds B's import without changing A's source.
5. B must either wait for A's proof/claim lifecycle, request a human exception, or
   publish a branch that fails the generated-root check.

The mathematical work can remain disjoint throughout this reproduction; the
shared generated file is what serializes publication.

Proposed direction

Give deterministic generated roots an explicit integration contract:

• Identify generated roots through a declared repository generator/output contract.
  A filename or header alone should not silently exempt handwritten code.
• The project integration coordinator regenerates them from the current tracked
  source inventory and current base after incorporating a checked candidate.
• Coordinate that bounded regeneration/integration operation with a short integration
  lease or queue. Proof workers retain their actual mathematical author claims
  without holding derived roots for the duration of unrelated proof work.
• Record the candidate/base/inventory/generator identity and apply the normal
  import-impact, cycle and repository checks to the resulting branch.
• Report the exact root, owner and supported handoff/integration action when a
  handwritten edit or incompatible generator makes this operation unsafe to automate.

Regeneration should reconstruct the complete root from the current inventory;
blindly merging stale generated patches or assuming that every import addition is
semantically harmless would lose the existing correctness checks.

Acceptance criteria

• Two independently checked, disjoint leaf batches can enter review without
  waiting for the other worker's entire proof-author lease.
• Regeneration on the latest tracked inventory preserves both workers' imports
  and is deterministic, including after a rebase or concurrent integration.
• Re-running an interrupted integration is idempotent; incomplete or stale
  generator output does not acquire publication authority.
• Handwritten roots, manual edits, deletions, duplicate declarations and import
  cycles retain their applicable author/impact/review checks.
• No live foreign claim is stolen, no mathematical gate is skipped, and no
  permanent global compiler lock is introduced.
• A small concurrent-worker regression fixture covers the scenario above, with
  diagnostics distinguishing proof completion from the actual publication blocker.

Scope and related work

• Formalize tracker: scalable orchestration, caching, verification and recovery #429: overall orchestration/caching/verification/recovery tracker.
• Formalize: long-lived work packages and durable session coordination #434: long-lived work packages and project coordination; the generated-root
  integration lifecycle described here is the specific publication gap.
• Skeleton: efficient report serialization and reusable review artifacts #433: immutable verification artifact reuse and serialization.
• Claims: bounded target-scoped status and listing diagnostics #432: bounded claim-status queries.
• Remove the claim board once no project relies on it #309: possible eventual claim-board removal. This issue addresses the current
  claims-enabled workflow and also needs a defined generated-file integration
  path if that board is removed.
• work import-impact checks and imports every root library for one import question #430: scoped import-impact loading; a generated root's forward closure can still
  cover a whole library, so this proposal does not assume that fix makes root
  integration cheap by itself.

Observed with Autoform 0.5.0 / installed commit
de6de5f029124533712dc82429e85b1d1ba75b1a and Lean 4.35.
Current main's claim instructions still retain the complete set through pushed
integration (checked at 53f84a05a77e3f0780e0735e0b618d3abee60554).
Repository root generation is consumer infrastructure; the proposed Autoform
change is its coordination/claim/integration protocol.

Reported by @toskua and Avocado.