[Vilin97]

OSforGFF repeatedly searches large arithmetic contexts and broad simplifier sets during its analytic proofs. This pass gives arithmetic tactics explicit premises, replaces nonlinear search by linear search where sufficient, and records the simplifier rules used by selected proofs. It also reuses Mathlib's Hadamard positivity and Hermitian results, proves fixed-time heat-kernel continuity directly from its scalar formula, factors a reflected-distance continuity lemma, and removes three redundant private imports.

Selected project: LeanPool.OSforGFF (88 modules, about 46,000 lines). Other large candidates included SpherePacking, DomainTheory, and SeveralComplexVariables; OSforGFF had substantial measured analytic proof costs and no competing optimization PR.

Base: 882795354c57bfed5c5fbbf950aa8ff840f4ff17. The selected project and pinned toolchain are unchanged on the newer main fetched before commit. This branch preserves the measured base rather than rebasing to chase unrelated merges.

The invariant and local checks pass. The source is under further optimization. Checkpoint 1880d47914d18786afdd2623ac0090a2245bd005 passed the invariant and checks with an 8.78% median wall reduction. Checkpoint 1225ea8293fd5422c4ad66c985e211402fccc0c9 also passes all audits; its next series was stopped after four successful builds because even the best remaining pair could not reach a 10% median reduction (baseline observations 577.23/557.17 seconds, optimized 536.81/526.92 seconds). All observations are retained. Additional compatible arithmetic rewrites have now passed the same metadata-erased invariant checker and all local checks at c91cefcfb73b15c005db6c77a0044dd4a7dd66cb, without relaxing semantic or source-statement checks. The next controlled series is in progress.

Invariant audit: before editing, a Lean environment inspector exported all 3,081 project declarations, including private/generated declarations, their fully elaborated types, universe parameters, safety, reducibility information, and every non-theorem value. After rebuilding the current head (3,390 total declarations), all pre-existing declarations compare identically after erasing kernel-irrelevant expression metadata. One existing generated matcher's only raw difference is source-location metadata. Theorem proof terms may differ. There are two new private continuity lemmas and 307 new generated proof-support declarations. Nineteen candidate proof owners were restored because they changed existing generated declarations. A separate source-signature comparison finds no changed or removed existing written declarations; the only two new written declarations are the private continuity helpers.

Validation completed:

• lake build LeanPool.OSforGFF.Imports, with the repository compiler/linter plugin; no warnings.
• lake --fail-level=warning build LeanPool.OSforGFF.Imports.
• lake exe runLinter --no-build --only-modules=../modules.txt LeanPool.OSforGFF.Imports: all 88 project modules, 3,386 declarations.
• lake exe lint-style LeanPool.OSforGFF.Imports.
• lake exe mk_all --module --check.
• Unmodified repository quality functions, scoped to all 88 project source files and its YAML card: headers, forbidden constructs, size, reachability, card/schema/declaration resolution; no findings.
• Repository axiom and compiled option/trust audits across every project module; no findings.
• lake shake --force --keep-public LeanPool.OSforGFF.Imports: removed the three redundant private imports; the remaining suggestions concern existing public imports, which are retained.
• git diff --check and the elaborated declaration manifest comparison.

Measurement method: delete only this project's local Lean/IR build outputs, keep pinned dependencies and tooling cached, then run taskset -c 12 env LEAN_NUM_THREADS=1 lake build LeanPool.OSforGFF.Imports under /usr/bin/time -v. Source digests, revisions, commands, and machine load are recorded for each run. The VM is shared. The completed first series has baseline wall times 625.66, 640.56, 634.93 seconds and optimized times 547.55, 579.18, 836.71 seconds. Medians are 634.93 → 579.18 seconds wall (8.78% faster) and 601.49 → 552.07 seconds CPU (8.22% lower). Median peak child RSS is 1,796,548 → 1,791,008 KiB. The slow final optimized run is retained. Further optimization and measurement are in progress. Current-head synchronous Lean command profiling of 11 representative modules (507 original declarations plus the two new private helpers, whose cost is included) shows 14.78% fewer raw heartbeat counts in aggregate. OS3MixedRepInfra improves from 2.46% below baseline at the first checkpoint to 11.80% below baseline after the additional pass.

GitHub’s advisory Proof Profile base and head jobs both failed during artifact restoration with No space left on device, before Lean measurement. The completed local profiles and timing data are independent of those jobs. No workflow changes or waivers are proposed.

Limits: this validates the selected project locally, not a rebuild of every other pool project. Protected CI and independent review remain required. No CI/configuration/gates, theorem statements, definition bodies, project card, or generated index are changed. No auto-merge is requested.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.