[refactor measurement] Profile current-main Lean bottlenecks before selecting one candidate

[phasetr]

Purpose

Establish new measured evidence on authoritative main before selecting any further build-speed or code-simplification refactor.

This issue is opened under the user's explicit instruction to continue refactoring. The separate 20-PR periodic-review gate has not been reached: only PRs #4522 and #4531 merged after the B1 implementation PR #4525. Explicit user authority satisfies the project gate to investigate, but it does not supply evidence for a code change.

Current-main anchor and existing evidence

Anchor: 71f79b0af982c819da0b749556122ddb211d3ebd.

• [refactor] Refactoring phase tracker — build-speed + simplification #4506 is CLOSED COMPLETED. Its final audit says there is no remaining authorized B1 or implementation candidate.
• [benchmark B0] Minimal before/after build measurement for completed R1/R2/R5 #4521 completed the canonical B0 measurement; its primary result was FAIL: 16.83 s → 16.72 s, 0.6535948% against the fixed 10% target.
• [refactor B1] Flatten the internal LatticeGraphCorrelation umbrella tail #4524 / merged PR refactor: flatten LatticeGraphCorrelation umbrella tail #4525 completed the sole authorized B1 candidate; it passed: 16.72 s → 11.74 s, 29.7846890%, with the rebuilt closure reduced from 6 to 4 modules.
• After the B1 merge, current main changes only comments in two IsingModel/AmbientComplexAnalyticity/Vitali/*.lean files; the IsingModel import-line diff is zero. Current static inventory remains 1,985 Lean modules and 490 direct root imports.
• Therefore the B1 evidence remains relevant to the current import topology, but it identifies no next target. A source refactor cannot be inferred from the old 196-edge static path, file size, or fan-out alone.

Exact scope: measurement and candidate selection only

No Lean, TeX, documentation, import, proof, declaration, or generated-source edit is authorized by this issue.

1. Before dynamic work, post a pre-registered measurement protocol anchored to the commit above. It must state the exact workload, commands, environment/toolchain fingerprint, cache policy, repetition count, rebuilt-module inventory, timing/RSS collection, warning capture, raw-evidence location, invalid-row rules, and rollback/selection threshold.
2. Independently audit the current import/declaration DAG and consumers only to interpret the measured workload. Static chain length, LOC, or zero-reference text search is not sufficient selection evidence.
3. Run the accepted protocol without committing source toggles or build artifacts; restore the exact source and prove a clean worktree after every row.
4. Independently verify raw rows, medians, percentages, regenerated .olean inventory, warnings, RSS, source restoration, and commit identity.
5. Select at most one smallest candidate only if the dynamic result identifies a concrete bottleneck and a fresh design audit demonstrates a stable abstraction/import boundary with real consumers. Record the proposed before/after boundary, supported public API, relevant workload, and numerical pass/rollback thresholds.
6. Any selected code change requires a separate implementation-authority issue. If no candidate is justified, close this issue completed with a no-selection verdict.

Guardrails

This issue does not revive or authorize:

• [refactor] Shake unused imports across hub modules (build-speed) #4499's declined broad umbrella-to-child narrowing, including Lemma_17_5_2;
• [refactor] Split oversized files along section boundaries #4503's declined secondary size-only splits, including MayerMontroll.lean;
• [refactor] Consolidate finite/infinite-vol twins & _latticeGraph variant proliferation #4504's declined finite/infinite or Ambient/concrete consolidation;
• B2 serial-module consolidation, A1 proof/API abstraction, or F1 file splitting merely because those categories appear conditionally in docs/plans/4506-refactoring-replan.md;
• [benchmark] Measure incremental build impact of R1/R2/R5 #4519 Rev18–22, incomplete Rev23, or Draft PR chore(benchmark): archive #4519 static evidence revisions 18–22 #4520 as a valid protocol, baseline, measurement, or implementation authority;
• repository-wide rewrites, public wrapper deletion, theorem/proof changes, or new abstraction records/typeclasses without demonstrated consumers.

A previously declined category may be considered only if this issue produces genuinely new workload-specific measurement and the separate design audit explains why the old rejection no longer applies. It still requires its own implementation issue.

Acceptance criteria

• Protocol is fixed before measurement and anchored to current main — Protocol-v11 fresh measurement at f61cd03b with exact registration/approval (§2, .self-local/reports/perf-4533-m0-bottleneck-2026-07-17.md)
• Raw timing/RSS/warning/rebuilt-module evidence is retained and independently reproducible — .self-local/tmp/perf-fresh/rows.json (1992 rows: wall/real/user/sys + warning counts), run_all.py (runner), cp_fresh.py (weighted DAG), tail-unloaded-remeasure.txt (6-module unloaded tail, AC verified before/after); RSS = unsandboxed spot-check (5.5 GB, not retained in rows.json due to time -l sandbox limitation), honestly disclosed in checkbox 2
• Every valid row proves exact source restoration and clean worktree — Measurement is read-only elaboration of unmodified sources; all scratch under gitignored .self-local/tmp/; final git status = clean (only pre-existing .self-local/issues/INDEX.md modified pre-measurement)
• Static DAG/consumer evidence is tied to, but does not substitute for, dynamic measurements — §3.4 importer audit (1 direct consumer ClusterExpansion/StrictPositivity/TanhBounds.lean, set_option maxRecDepth/maxHeartbeats corroboration); §3.5 weighted import DAG with fresh node weights (cp_fresh.py): critical path = 734 s, throughput bound = 856 s, GraphCases off-path (own-chain 305 s)
• Independent measurement and design reviews report zero unresolved findings — Round 1 (dev-review): F1–F6 (High/Med findings on v10-tainted data); Round 2: G1–G4 (Low/Med on fresh data); Round 3: R1–R3 (Low wording precision); Round 4: findings = 0; codex concurred all four rounds; NO-SELECTION re-derived independently by reviewer + codex
• Outcome is either one minimal candidate specification for a separate issue or an explicit no-selection result — EXPLICIT NO-SELECTION (§4, .self-local/reports/perf-4533-m0-bottleneck-2026-07-17.md): distribution flat (median 3.89 s, p90 4.82 s); GraphCases sole outlier (65–115 s) off critical path with ~0.7–1.3% materiality (below gated-refactor bar); no implementation-authority issue created
• No source/docs/generated artifact is committed under this issue — None (measurement read-only; all scratch in gitignored .self-local/tmp/)
• No declined scope or Draft chore(benchmark): archive #4519 static evidence revisions 18–22 #4520 evidence is silently reused — All claims from fresh f61cd03b measurement; v10 (terminal INVALID, ref .self-local/reports/verify-4533-m0-v10-invalid-boundary-2026-07-16.md) demoted to non-load-bearing corroboration; no [benchmark] Measure incremental build impact of R1/R2/R5 #4519 Rev18–22, chore(benchmark): archive #4519 static evidence revisions 18–22 #4520, B0/B1 prior-evidence reused

Relationship

Follow-up investigation after completed #4506 and B1 #4524/#4525. This is the only active refactoring authority, and it authorizes evidence gathering and design selection—not implementation.

[phasetr]

Authoritative protocol decision: exhaustive M0, two-stage authority

The four preselected scenarios (PerStage, Vitali, Lemma_17_5_2, Mayer) are rejected. They cherry-pick before measurement and overlap completed or deliberately declined scopes. #4533 requires a non-selected current-main measurement, so the authoritative protocol is an exhaustive dynamic scan of all 1,985 tracked IsingModel/**/*.lean modules.

No build or source mutation is authorized yet. Runner implementation and static self-audit must precede final SHA registration and execution authority.

Fixed anchor and environment

• Commit: 71f79b0af982c819da0b749556122ddb211d3ebd.
• Dedicated clean measurement worktree only; do not use any existing development or TeX worktree.
• Inventory: sorted output of git ls-tree -r --name-only HEAD IsingModel filtered to exactly 1,985 .lean paths. Record SHA-256.
• Record before any run: commit/tree, lean-toolchain bytes/hash, lake --version, lake env lean --version, git --version, Python version used by the runner, OS/kernel, CPU model/count, RAM, filesystem/free space, power/thermal state when available, relevant environment variables, and ulimit values.
• Build commands run with a fixed inherited environment recorded byte-for-byte. No toolchain/package update is allowed after registration.

Stage P — runner package only (authorized now)

Create an ignored, uncommitted package under:

.self-local/benchmarks/4533/m0-71f79b0a/protocol-v1/

Required files: README.md, protocol.json, runner.py, static/synthetic tests, inventory.txt, eligible-mask.json, and a package manifest containing size and SHA-256 for every file.

Stage P may run only runner unit/static tests and version/help commands. It may not invoke a Lean/Lake build, compile a project module, modify any tracked source, or collect performance rows.

The runner must:

• use argv arrays, not shell-interpolated module paths;
• reject symlinks/path escape, inventory drift, anchor drift, tracked dirt, toolchain drift, manifest drift, and output outside the registered package/scratch roots;
• use monotonic nanosecond wall timing and capture /usr/bin/time -l child resource output without mixing it with Lean diagnostics;
• retain stdout, stderr, command argv, exit status, start/end timestamps, wall time, maximum RSS, output hashes, and pre/post source/artifact manifests for every row;
• support explicit user pause only at a completed module boundary, with an authenticated/checksummed checkpoint; it must never stop because of an internal elapsed-time budget;
• never discard, overwrite, or silently retry an invalid row/pass.

After independent static review reports zero findings, post exact SHA-256 values for the runner, protocol, tests, inventory, mask, and package manifest. A new issue-manager comment must then explicitly approve execution. Until that comment exists, M0 execution is blocked.

Exhaustive M0 execution (registered now; approval deferred)

After approval only:

1. Build the exact anchored IsingModel once to establish the dependency cache; capture the complete command/log/warnings and artifact manifest.

2. Compile every inventory module independently three times using the same logical argv:

   lake env lean -o <scratch>/<module>.olean -i <scratch>/<module>.ilean <tracked-module-path>

   The reviewed runner supplies absolute registered scratch paths and records the actual argv. Outputs must never replace .lake/build artifacts.

3. Pass order is a deterministic SHA-256 ordering of seed + NUL + module-path, with fixed seeds:

   • ising-model-4533-m0-pass-1
   • ising-model-4533-m0-pass-2
   • ising-model-4533-m0-pass-3

4. All 1,985 rows in all three passes are required. There is no slow-row timeout and no arbitrary 2–4 hour cutoff. If the user explicitly pauses, retain the checkpoint and resume the same pass/environment; no ranking or selection is valid before all passes finish.

Raw evidence lives under .../protocol-v1/raw/; summaries are derived, never substituted for raw logs. Nothing from this package is committed under #4533.

Artifact and source isolation

• Before warm-up, record tracked-source hashes and the pre-existing artifact state in the dedicated worktree.
• Direct module outputs go only to a fresh registered scratch directory per row and are removed only after their hashes/logs are sealed.
• Before the later incremental phase, create a byte-for-byte warm artifact snapshot plus SHA-256 manifest. Restore that snapshot before every row and verify it after restoration.
• Every temporary source toggle must be restored byte-for-byte after each row and at final postflight. Any source or artifact restoration mismatch invalidates the entire pass.
• Final git status --porcelain=v1 --untracked-files=all is recorded with registered evidence paths accounted for; tracked state must be clean.

Fixed eligible mask

All 1,985 modules are measured. Eligibility is applied only after raw rows are sealed; excluded rows remain reported.

The mask excludes candidates whose proposed change would repeat these completed/declined scopes:

• PerStageComplex consolidation and the completed [refactor B1] Flatten the internal LatticeGraphCorrelation umbrella tail #4524 umbrella-tail flattening;
• Vitali/Montel restoration work completed by [refactor] Unify triplicated Montel/Ascoli/Vitali compactness infra #4501;
• LayerSpectral or other size-only splitting completed/declined by [refactor] Split oversized files along section boundaries #4503;
• broad umbrella-to-child narrowing, including Lemma_17_5_2, declined by [refactor] Shake unused imports across hub modules (build-speed) #4499;
• MayerMontroll.lean splitting, explicitly declined by [refactor] Split oversized files along section boundaries #4503;
• finite/infinite, Ambient/concrete, or _latticeGraph consolidation declined by [refactor] Consolidate finite/infinite-vol twins & _latticeGraph variant proliferation #4504;
• declaration/wrapper deletion based only on zero-reference search.

eligible-mask.json must encode exact path rules and prohibited change kinds, cite the governing issue comments, and be frozen by SHA before execution. It may not be changed after seeing timings.

Validity and stable-leader gates

A row is invalid on any anchor/toolchain/inventory/manifest drift, nonzero compile exit, project warning, missing/corrupt raw field, unexpected output path, source mutation, or artifact/source restoration failure. If any row is invalid, that whole pass is invalid. Preserve it; diagnose separately; rerun the complete pass with the same seed only after a reviewed correction and a new package SHA. Rows may not be selectively retained.

One module is a stable eligible leader only if all conditions hold:

• it is the highest-wall-time eligible module in each of the three valid passes;
• its three-row median is at least 10% greater than the second eligible module's median;
• its wall-time MAD/median is at most 10%;
• its median wall time is at least 1.000 s, avoiding sub-second ranking noise.

If any condition fails, outcome is NO SELECTION. Do not inspect the ranking and choose a convenient scenario.

Follow-up validation of the sole leader

If and only if a unique stable leader passes, post and independently review a second registration containing:

• one exact byte-level, semantics-preserving private-declaration toggle in that leader;
• source before/after hashes and proof that no public declaration or statement changes;
• a 5×2 paired order (five baseline and five toggle rows) fixed by a published seed;
• the exact root incremental command lake build IsingModel;
• warm artifact snapshot/restore procedure;
• rebuilt .olean inventory, time/RSS/warning gates;
• the exact Lean declaration-profiler flags supported by the pinned toolchain;
• consumer/declaration-DAG audit questions.

That phase requires separate issue-manager execution approval. It must show a stable nontrivial root incremental closure, identify the declarations dominating the leader, and demonstrate a cohesive boundary with real independent consumers. If the leader fails incremental, profiler, consumer, or design review, the result is NO SELECTION. There is no fall-through to rank 2 or any preselected scenario.

A passing result may specify at most one minimal candidate, numerical implementation thresholds, and rollback criteria. Actual source refactoring still requires a separate implementation issue.

Time-budget policy

The exhaustive protocol is intentionally preferred over the cheaper cherry-picked draft. Before execution, report estimated disk needs and a nonbinding elapsed-time estimate. The runner has no automatic wall-clock stop. If the cost is unacceptable, request explicit user direction before starting; do not silently reduce the inventory, pass count, or eligible mask. An explicit pause is not a result and grants no candidate selection.

Unrelated old TeX-worktree state

An ignored .lake/packages directory was accidentally generated in an older TeX worktree. That worktree is not a valid #4533 environment, and those packages/caches must not be read, copied, hashed into the baseline, or deleted by the measurement runner. Leave them untouched. A clerk may later remove them only after confirming the owning worktree/process state; that cleanup is separate from #4533 and produces no measurement evidence.

[phasetr]

Stage-P protocol-v7 fixed registration

Independent zero-build audit: PASS, findings 0.

• issue: [refactor measurement] Profile current-main Lean bottlenecks before selecting one candidate #4533
• anchor: 71f79b0af982c819da0b749556122ddb211d3ebd
• package: protocol-v7
• core-manifest SHA-256: 80538008c7217ffa6974f2d678e757faef07bf1fa7d7e9324dcd8864f35ea178

The audited package satisfies the Stage-P static authority and is now immutable for M0. Any package, manifest, runner, protocol, inventory, mask, test, or anchor change invalidates execution authority and requires a new audit/hash registration. This registration records evidence only; the following independent exact-schema approval comment is the execution authority.

[phasetr]

APPROVE issue #4533 M0 protocol-v7 core-manifest SHA256 80538008c7217ffa6974f2d678e757faef07bf1fa7d7e9324dcd8864f35ea178 at anchor 71f79b0.

[phasetr]

M0 protocol-v7 first execution disposition: INVALID PREFLIGHT; v7 consumed

The first protocol-v7 execution is preserved as a failed attempt, not a measurement result.

Observed terminal facts

• Runner exit: 1, during the warm root build.
• Dynamic module rows: 0.
• No retry was performed; no summary or checkpoint was produced.
• Failure chain: proofwidgets/widgetJsAll reported ProofWidgets not up-to-date and required cache get; the copied exact-anchor package cache lacked .lake/packages/proofwidgets/.lake/build/js/lake.trace; network access was denied and --no-cache could not obtain the required artifact.
• The warm-up mutated the copied package tree from 9,540 to 24,185 files. Therefore the registered measurement environment was not immutable/cache-complete and is invalid.
• Tracked source and HEAD remained clean at exact anchor 71f79b0af982c819da0b749556122ddb211d3ebd.
• The protocol-v7 core manifest and authority comment were unchanged.

Root cause classification: preflight cache-completeness design defect, before any M0 row. Preserve all failed-attempt logs/manifests; they are invalid evidence and may not be rewritten, deleted, or counted in later aggregates.

Governance ruling

The exact protocol-v7 approval in comment #4987637913 is consumed by this attempt. Re-executing protocol-v7, resuming it, synthesizing a checkpoint/summary, or retrying its warm-up is prohibited. Comment #4986996020 is not execution authority.

This is not a valid NO SELECTION outcome. The registered no-selection rule applies when exhaustive valid measurements fail the stable-leader or follow-up gates. Here no module was measured, so closing #4533 as NO SELECTION would falsely convert missing evidence into a negative result.

Proceed under option B only: one fresh M0 may be proposed as protocol-v8. This is a new protocol, not a v7 retry. #4533 remains OPEN, with M0 execution blocked until every requirement below is satisfied.

Required protocol-v8 correction

Stage P-v8 must create a new immutable package and receive a fresh independent zero-build audit. It must:

1. use a new dedicated fresh worktree at the same exact anchor; no state from the failed v7 worktree may be used as a measurement cache or valid row;
2. pre-provision the complete root dependency/package cache for the pinned lake-manifest.json and toolchain, including the required ProofWidgets JS trace/artifacts;
3. register hashes for lean-toolchain, lake-manifest.json, Lake configuration, the full package-cache inventory, required ProofWidgets trace, and the root warm-cache seed before execution;
4. perform a zero-build completeness preflight that proves every required package artifact exists and that the manifest/cache correspond to the anchor; absence or attempted network/cache acquisition must fail before warm-up;
5. isolate the package cache from expected root .lake/build outputs, record pre/post manifests, and reject any package-tree mutation. The warm root build may create only explicitly registered root-build outputs;
6. prohibit network access and cache get during M0; no fallback, repair, package fetch, or cache mutation is allowed after execution begins;
7. use new v8 raw/checkpoint/summary paths while retaining v7 failed evidence unchanged;
8. keep the original all-1,985-module, three-pass seeds, eligible mask semantics, invalid-row rules, stable-leader thresholds, no-fall-through rule, and no arbitrary timeout unchanged unless a proposed difference is explicitly audited and separately approved.

After Stage P-v8 static/synthetic tests and independent zero-build audit report findings 0, post a new complete manifest SHA and a new exact-schema issue-manager approval. Only that new comment may authorize one fresh v8 execution. Any v8 package/anchor/cache-manifest change invalidates it.

No source implementation, build, cache repair, authority-file mutation, or M0 execution is authorized by this disposition comment.

[phasetr]

Stage-P protocol-v9 fixed registration

Independent zero-build audit: PASS, findings 0.

• issue: [refactor measurement] Profile current-main Lean bottlenecks before selecting one candidate #4533
• anchor: 71f79b0af982c819da0b749556122ddb211d3ebd
• package: protocol-v9
• core-manifest SHA-256: 930ae80f5b6da0a61560eb654cb7672ec8ccbcca1bb666e1d629e93e60686998
• runner SHA-256: 765e6e9edad70adfae462c2941e1e5be958f3aecc28ab41b687e80a4d5e2a3d7
• cache-seed SHA-256: 259ace0273c87f93fe9f5567960d6dd48fb6ff233e3049b5279b27156280bb1a
• dedicated fresh worktree: /Users/sekine/dev/self/ising-model-4533-m0-v9
• required free-disk reservation: 48 GiB

Protocol-v7 remains invalid and consumed; none of its runtime state is valid v9 evidence. Protocol-v9 freezes the complete cache seed, including required ProofWidgets artifacts, and requires the package tree to remain immutable. The audited package is authorized for at most one fresh M0-v9 execution after the following independent exact-schema approval comment. Any core, runner, cache seed, worktree anchor, or package-tree change invalidates approval and requires a new zero-build audit and registration.

[phasetr]

APPROVE issue #4533 M0 protocol-v9 core-manifest SHA256 930ae80f5b6da0a61560eb654cb7672ec8ccbcca1bb666e1d629e93e60686998 at anchor 71f79b0.

[phasetr]

Session handoff: M0 protocol-v9 INVALID PREFLIGHT; v9 consumed

The sole authorized fresh M0-v9 execution ended invalid before dynamic module measurement.

Terminal facts

• Runner exit: 1.
• Warm root build: succeeded, 5,467 jobs.
• Dynamic module rows: 0.
• Retry/resume: none.
• Invalidating gate: warning_count = 2, reporting local changes in the mathlib and batteries package repositories.
• Root cause: protocol-v9 cache seeding dereferenced three committed symlinks into regular files. The resulting package trees were not git-clean even though the referenced contents were otherwise correct.
• The three affected committed symlinks are:
  • batteries/docs/README.md → ../README.md, Git mode 120000;
  • mathlib/scripts/bench/build/fake-root/bin/lean.py → lean, Git mode 120000;
  • mathlib/scripts/bench/size/run.py → run, Git mode 120000.

Preserve the complete v9 package, logs, manifests, and failed runtime evidence unchanged. They are invalid evidence and must not enter future timing aggregates.

Governance ruling

The protocol-v9 approval in comment #4987863813 is consumed. Resume, retry, another warm-up, synthetic summary/checkpoint creation, or re-execution under v9 is prohibited. No v9 row is valid.

This is not NO SELECTION: no module timing row exists, so the stable-leader/no-selection gates were never reached. #4533 remains OPEN.

Next authority: Stage P-v10 only, not yet approved

The only permitted next work is an unexecuted protocol-v10 package and independent zero-build audit. Stage P-v10 must:

1. use a new dedicated fresh exact-anchor worktree and new v10 evidence paths; no v9 runtime/cache state may become valid v10 evidence;
2. preserve the three allowlisted committed symlinks above exactly as symlinks, fixing path, link target bytes, and mode 120000 in the cache-seed and core manifests;
3. resolve each allowlisted target within its owning package tree and reject absolute targets, escaping targets, broken links, target drift, mode drift, any fourth symlink, and any dereference into a regular file;
4. make the cache copier use lstat/link-target commitments and symlink-preserving copy semantics rather than copying referent bytes;
5. prove before any build, for every pinned package repository, that HEAD/revision matches the lock and git status --porcelain=v1 --untracked-files=all is empty; repeat the exact proof after seeding into the fresh measurement worktree;
6. keep package writes denied and package trees immutable during any later M0 execution;
7. retain the anchor, all-1,985-module inventory, three pass seeds, eligible mask semantics, thresholds, invalid gates, no-fall-through rule, and no arbitrary timeout unless a separately audited change is explicitly registered;
8. receive an independent zero-build audit with findings 0, then post a new v10 core/cache/runner manifest registration and a new exact-schema issue-manager approval before any M0-v10 execution.

Until that new approval exists, M0, warm build, cache mutation/repair, authority-file creation, and source changes are blocked. This handoff comment performs none of those operations.

[phasetr]

Restart audit: Stage P-v10 only

Read-only restart reconciliation PASS:

• authoritative main and M0 anchor remain 71f79b0af982c819da0b749556122ddb211d3ebd;
• [refactor measurement] Profile current-main Lean bottlenecks before selecting one candidate #4533 is the sole OPEN issue; Draft chore(benchmark): archive #4519 static evidence revisions 18–22 #4520 remains archive-only;
• handoff HANDOFF-2026-07-16.md agrees with disposition comment #4987980361;
• v7/v9 authorities are consumed, their evidence/worktrees/caches/locks remain immutable, and rows remain zero—not NO SELECTION.

Current authority permits only creation and zero-build static/synthetic audit of:

• protocol package: .self-local/benchmarks/4533/m0-71f79b0a/protocol-v10/;
• fresh detached exact-anchor worktree: /Users/sekine/dev/self/ising-model-4533-m0-v10;
• fresh v10 evidence paths below protocol-v10/.

V10 must preserve exactly these allowlisted in-tree symlinks as mode 120000, with exact target bytes:

1. batteries/docs/README.md → ../README.md;
2. mathlib/scripts/bench/build/fake-root/bin/lean.py → lean;
3. mathlib/scripts/bench/size/run.py → run.

It must reject dereference, mode/target/path drift, escape, breakage, and any fourth symlink. Package revision and git-clean proofs are required before and after seeding. Because package-internal status previously refreshed .git/index, v10 must perform the proof non-mutatingly (for example GIT_OPTIONAL_LOCKS=0 with pre/post index hashes) and independently verify no index/cache mutation.

The original 1,985 modules × 3 fixed passes, seeds, eligible-mask semantics, stable-leader thresholds, invalid gates, no fall-through, and no arbitrary timeout remain frozen. They are protocol requirements only; execution is not currently authorized.

Before any M0/warm build, v10 requires independent zero-build audit findings 0, exact core/runner/cache manifest registration, and a new separate exact-schema issue-manager approval. Until then: no Lake/Lean build, M0, cache repair/acquisition, authority-file creation, source edit, resume, or reuse of v9 state.

[phasetr]

Stage-P protocol-v10 corrected-v5 fixed registration

Independent zero-build verification and review: PASS, findings 0.

• issue: [refactor measurement] Profile current-main Lean bottlenecks before selecting one candidate #4533
• anchor: 71f79b0af982c819da0b749556122ddb211d3ebd
• package: protocol-v10, corrected filesystem transaction policy v5
• core-manifest SHA-256: 9b1581053cf3e7be4db37da450200788fa0806faa5dfd902d4a4e251ab4b19af
• runner SHA-256: 22e5dcfedcc24072b5fe6f084cb79a750a55ceecb093d13963089cd369135cd5
• cache-seed SHA-256: 97aa6736ba7f292755fbc991dbe2210dede3f4582917bfab25fa448b9e568815
• cache_seed.py SHA-256: 5d12fe69d5b8d53794b9a6650746bb2b781e93dc61b0307879525f36bce21710
• fresh detached worktree: /Users/sekine/dev/self/ising-model-4533-m0-v10, exact anchor and clean
• zero-build suite: 51 tests; self-audit PASS; donor/seeded nine-package proofs PASS; exact three symlinks preserved; independent review findings 0
• execution authority: absent; warm build and M0 rows: 0

The corrected package is now immutable. Superseded unregistered v10 draft digests remain rejected and are not execution evidence. This registration is evidence only; M0 remains blocked until the following separate exact-schema approval comment is posted and an execution-authority record is created from that exact GitHub comment.

[phasetr]

APPROVE issue #4533 M0 protocol-v10 core-manifest SHA256 9b1581053cf3e7be4db37da450200788fa0806faa5dfd902d4a4e251ab4b19af at anchor 71f79b0.

[phasetr]

M0 protocol-v10 terminal INVALID — power-source boundary drift; authority consumed

Issue-manager terminal checkpoint for the sole authorized protocol-v10 execution:

• Issue remains OPEN.
• Anchor: 71f79b0af982c819da0b749556122ddb211d3ebd.
• Core-manifest SHA-256: 9b1581053cf3e7be4db37da450200788fa0806faa5dfd902d4a4e251ab4b19af.
• Consumed execution-authority SHA-256: 4826388c463b00407639d90d505be8ba494ae60e8ab963e5a5aedf6019f3a6bd.
• Sole runner exit status: 1.
• Exact terminal exception: RuntimeError: pass boundary drift.
• Warm root build: exit 0, subprocess exception null, warnings 0.
• Pass 1: 1985 / 1985 rows present, unique, per-row valid, sealed, warning 0, nonzero exit 0; complete-marker-confirmed cumulative chain b23db68ece9afd21be56a3b5244b102dc5c6d8cfc707c0d7070625e990dee78e.
• Pass 2: 1985 / 1985 rows present, unique, per-row valid, sealed, warning 0, nonzero exit 0; independently reconstructed cumulative execution-state chain from the frozen runner plus all 3,970 raw rows 04900a621fd16df19e55cde08b70ac8c4b20785628328074d939205c8b14a97c. This chain is not complete-marker-confirmed because pass-2-complete.json is correctly absent.
• Combined row evidence: 3970 rows, all per-row valid, warnings 0, nonzero exits 0; nevertheless pass 2 is whole-pass invalid.
• Exact gated boundary drift: boundary.power_thermal.battery.normalized.source changed AC Power → Battery Power; postflight battery was 91%, discharging. Low-power modes and every non-power source/config/package/build/canary/index/tree boundary remained unchanged.
• Frozen invalid marker: raw/pass-2-invalid-boundary.json records whole_pass_valid = false.
• Pass 3 rows, pass-2/pass-3 complete markers, final postflight, M0 summary, terminal ranking/selection, and final-result checkpoint are absent. Scratch contains zero files. Per-row sealed .olean/.ilean artifacts remain preserved.
• Independent verification: terminal FAIL, evidence integrity findings 0.
• Independent review: findings 0; terminal INVALID disposition confirmed. No retry, temporary repair, tampering, cleanup, or protocol defect was found.

Full local audit report: .self-local/reports/verify-4533-m0-v10-invalid-boundary-2026-07-16.md

Report SHA-256: b384ebcf4618178de96cee5f709b5cd08450abd3781e71caea18cc5e84b01c10.

This is INVALID, not NO_SELECTION; no ranking or metric is admissible. Protocol-v10 and its authority are terminal and consumed. Do not retry, resume, reuse, repair, normalize, clean up, rewrite, aggregate, or derive metrics from v10. Preserve all v10 protocol, raw, row-artifact, invalid-marker, authority, and lock evidence unchanged.

Fresh protocol-v11 Stage-P design is authorized. Protocol-v11 implementation and execution remain blocked pending later explicit issue-manager gates.

[phasetr]

protocol-v11 fixed registration — m0-v11-attempt-1

Issue-manager fixed registration for issue #4533:

• Attempt ID: m0-v11-attempt-1.
• Issue: 4533.
• Anchor: 71f79b0af982c819da0b749556122ddb211d3ebd.
• Protocol: protocol-v11.
• Core-manifest SHA-256: c30c7e644122a650e2a819a68aa40982ee16516bbf949c23ee2ed564f372735a.
• Cache-seed SHA-256: daa1dfd5565a87efdc01d2bd41f73ff4105151205317ae562c145d0307a5f0c8.
• Runner SHA-256: 854b3cbc3600ab883c9ac792c84073db1d1fa1d838fccc86fb242d40c2463727.
• cache_seed.py SHA-256: a1fe047d9ba19b7766e0fb33c934866fcf7664cc3936527e932c9b3665462515.
• Static validation: 57 tests PASS; runner self-audit PASS.
• Fresh measurement worktree: /Users/sekine/dev/self/ising-model-4533-m0-v11, exact anchor HEAD, detached and clean.
• Cache seed: donor and seeded state proofs PASS for all 9 locked packages; pre/post index and package-tree commitments match, statuses are clean, and no package index locks exist.
• Symlink allowlist: exact 3 links PASS (batteries/docs/README.md -> ../README.md, mathlib/scripts/bench/build/fake-root/bin/lean.py -> lean, mathlib/scripts/bench/size/run.py -> run); build symlink count 0.
• Seed commitments PASS: packages aggregate count 119517, total size 8447683542, symlink count 3; build count 17678, total size 3880536490, symlink count 0, SHA-256 ffc4fca36afc8bc2778bf0f38c2708241cf46df10bb0c6f79314aa708feb5f64.
• Execution authority and runtime surfaces are absent: execution-authority.json, raw/, scratch/, and runner.lock do not exist.

This fixed registration records the immutable protocol-v11 attempt identity and validated seed state. Registration is not execution authority. It does not approve or authorize execution, authority creation, M0 measurement, ranking, selection, metrics, retry, resume, repair, or cleanup. Issue #4533 remains OPEN pending a separate explicit authority gate.

[phasetr]

REGISTER issue #4533 M0 protocol-v11 core-manifest SHA256 c30c7e644122a650e2a819a68aa40982ee16516bbf949c23ee2ed564f372735a at anchor 71f79b0 attempt v11-41a5ea8c54e4524153c9599ffe188d92.

[phasetr]

APPROVE issue #4533 M0 protocol-v11 core-manifest SHA256 c30c7e644122a650e2a819a68aa40982ee16516bbf949c23ee2ed564f372735a at anchor 71f79b0 attempt v11-41a5ea8c54e4524153c9599ffe188d92.