[kim-em]

Use meta imports for ImportGraph and LeanSearchClient, and add regression tests following #43912. After public import Mathlib, ordinary runtime definitions using representative APIs must fail, while corresponding meta definitions succeed. An explicit ordinary ImportGraph import enables its representative runtime definition.

The tests explicitly document that they check representative declarations: they do not guarantee that other declarations have not become available at runtime. LeanSearchClient already marks its representative declaration meta upstream, so its test checks that API's phase rather than detecting ordinary imports. These tests do not prevent theorem statements about dependency types.

---

Related to #43912; this PR is independent and targets master.

Validation:

• Rebuilt Mathlib.Tactic.Common, Mathlib.Tactic.DuplicateDecls, and Mathlib.Tactic.Linter.UpstreamableDecl.
• lake env lean MathlibTest/ImportDevTools.lean and lake env lean MathlibTest/ImportDevToolsExplicit.lean passed.
• Confirmed that the negative ImportGraph test fails against unmodified master artifacts.
• lake exe lint-style Mathlib Archive Counterexamples Wanted passed.

🤖 Prepared with Codex

[github-actions]

PR summary 3f672c49f7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ importGraphExplicit
+ importGraphRuntime
+ leanSearchRuntime

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 3f672c4).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 3f672c49f7
Reference commit 5b040b83e2

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[grunweg]

I don't understand the second sentence. Can you rephrase, please?