refactor: drop twelve dead pseudoMassG decoration lemmas

[phasetr]

Summary

The user gave explicit item-specific authorization to delete reference-0 declarations. IsingModel/PseudoMass/Profile.lean was reported as having 22 of its declarations unreferenced across the repository, but an independent audit narrowed that to 12: seven of the original candidates are load-bearing inside the file (they feed declarations that live modules consume, e.g. pseudoMassG_analyticAt → analyticWithinAt_Ici_zero → Lemma_17_5_2/UniformTransferLargeK.lean), and three are cited by docs/index.md as GJ §17.5 results in their own right (one_div_mul_pow_mul_one_div_mul_pow_eq at :2050, one_div_one_add_pow_mul_one_div_one_add_pow_le_one_div_pow_mul_one_div_pow at :2052, pseudoMassG_le_two_div_one_add_pow_of_preimage_le at :1943). Only the remaining 12 are deleted here.

Context

This completes on the pseudoMassG layer the same dead-decoration sweep that PR #4536 (1793e549) already performed on the pseudoMassExt layer, where the exact twins of several of these lemmas (neg_pseudoMassExt_strictMonoOn, pseudoMassExt_lt_iff, pseudoMassExt_differentiableOn, pseudoMassExt_continuousOn) were removed. Some of the candidates lost their last consumer in that very PR.

Scope

Eight leaves plus four that become unreferenced once the leaves go — they must be deleted together, or the four become new dead declarations.

Note that none of the twelve is cited by docs/index.md or tex/proof-guide.tex, so no documentation update is expected; this will be re-verified during implementation.

Note on pseudoMassG_analyticAt_of_even (raised by codex review)

One of the twelve, pseudoMassG_analyticAt_of_even, is not a redundant special case of the
surviving pseudoMassG_analyticAt. It claimed AnalyticAt ℝ (pseudoMassG α r) t for all
t : ℝ when α is even (using boundedness of (t·r)^α ≥ 0 to keep the denominator positive
everywhere), whereas pseudoMassG_analyticAt only covers r > 0, t ≥ 0. It is a genuinely
broader (all-of-ℝ) statement, just an unused, standalone one — no open GJ §17.5 target requires
analyticity for t < 0. Deletion is still correct (zero references anywhere), but it is a
deletion of an independent unused result, not a "duplicate discard."

Verification checklist

• The twelve names have no remaining references anywhere (rg over IsingModel/, docs/, tex/, test/, scripts/)
• lake build warning-free
• scripts/audit_gate.py V1-V4
• lake exe GKSTest
• #print axioms unchanged for the surviving declarations in the file
• No new reference-0 declarations created by the deletion
• CI green

Resolves #4640

🤖 Generated with Claude Code

[phasetr]

dev-issue-manager: pre-merge resolution verification (PASS)

Verified independently against HEAD 0b7e70fe (not merely re-stating the three-gate reports):

• CI: build check = SUCCESS (run 29791889669, 9m6s). Only one required check configured; it is green.
• 12 deleted names confirmed zero references anywhere in IsingModel/, docs/, tex/, test/, scripts/ (independent rg/grep, not trusted from dev-verify's report).
• 10 protected declarations verified present in IsingModel/PseudoMass/Profile.lean at HEAD:
  • 3 docs-cited survivors confirmed at their docs/index.md citation lines: one_div_mul_pow_mul_one_div_mul_pow_eq (:2050), one_div_one_add_pow_mul_one_div_one_add_pow_le_one_div_pow_mul_one_div_pow (:2052), pseudoMassG_le_two_div_one_add_pow_of_preimage_le (:1943).
  • 7 load-bearing survivors confirmed alive via internal dependency closure; spot-checked the pseudoMassG_analyticAt → pseudoMassG_analyticWithinAt_Ici_zero → (external) Lemma_17_5_2/UniformTransferLargeK.lean chain directly in source (Profile.lean:511-524, external consumer confirmed by grep).
• File: 745→610 lines, deletion-only diff (git diff main...HEAD -- IsingModel/PseudoMass/Profile.lean = 135 deletions, 0 insertions). No sorry/admit/native_decide in the file.
• PR refactor: remove 97 dead decoration lemmas + 2 unused imports (2026-07-17 tier2 cycle) #4536 correspondence: confirmed — refactor: remove 97 dead decoration lemmas + 2 unused imports (2026-07-17 tier2 cycle) #4536 (merged 1793e549) removed the pseudoMassExt-layer twins of several of these lemmas, establishing the precedent this PR completes on the pseudoMassG layer.

codex even-α finding: the deleted pseudoMassG_analyticAt_of_even claimed AnalyticAt ℝ (pseudoMassG α r) t for all t : ℝ (even α), which is strictly stronger than the surviving pseudoMassG_analyticAt (r > 0, t ≥ 0 only) — not a special case of it, a genuinely different (broader-domain) statement. Since it has zero references anywhere and no open GJ §17.5 target requires all-of-ℝ analyticity (only t ≥ 0 is used downstream), deletion is correct; codex's point is accurate as a mathematical observation but non-blocking for this PR. Recommend a one-line note in the PR body/commit trailer so future dead-sweep audits don't misread the deletion as removing a "duplicate" of pseudoMassG_analyticAt (it wasn't — it was a broader, unused, standalone result).

Verdict: resolved. No unresolved/mis-stated items found. Merge-ready.