refactor: drop a duplicated pseudoMassFromParamsAtPair J=0 h=0 lemma

[phasetr]

Motivation

Simplification refactor under the user's standing authorization, continuing the scanner-vetted deletions of #4636/#4641/#4648/#4651/#4655. Two theorems state the identical proposition — pseudoMassFromParamsAtPair hα hr d Λ ⟨0,0,β⟩ x z = 0 under the same hypotheses (hα, hr, d, Λ, edge-Fintype instance, 0 < β, arbitrary x z) — a duplicate proof of one fact:

• pseudoMassFromParamsAtPair_J_zero_h_zero (IsingModel/PseudoMass/FromParamsBasic/BasicSlices.lean:105)
• pseudoMassFromParamsAtPair_J_zero_h_zero_any_pair (IsingModel/PseudoMass/FromParamsHZero/JZeroValues.lean:61)

Both are referenced nowhere in the repository outside their own declaration, and neither is cited by docs/index.md or tex/proof-guide.tex.

Decision: which to delete

Per the issue #4639 adoption rule, when both candidates are reference-0 only one is removed. The JZeroValues hub (_any_pair) is kept and the BasicSlices direct copy (_J_zero_h_zero) is deleted, because:

• _any_pair is the canonical "J-zero value cases" module head and case-splits (x = z / x ≠ z) into the granular helpers pseudoMassFromParamsAtPair_diag_h_zero and pseudoMassFromParamsAtPair_at_J_zero_h_zero_eq_zero, which are referenced only by _any_pair.
• Deleting _any_pair would cascade those two helpers into new reference-0 declarations. Deleting the BasicSlices direct copy (whose proof uses only general library lemmas — correlationInfinite_J_zero, pseudoMassExt_of_not_mem) leaves the dependency graph intact.
• The two statements are literally identical (same binders, same conclusion), so keeping _any_pair loses no information.

Post-deletion the two helpers remain load-bearing (scanner re-run) → cascade = 0.

Scanner output (issue #4639 adoption rule)

python3 scripts/dead_candidate_scan.py --name pseudoMassFromParamsAtPair_J_zero_h_zero --name pseudoMassFromParamsAtPair_J_zero_h_zero_any_pair --lean:

--lean cross-check: 2 candidate(s) compared against the elaborated graph; no consumer seen by Lean was missed on a safe-to-delete verdict
== dead-candidate scan ==
canary: 1096 declarations carrying 'Λ'x1093, 'β'x1, 'σ'x2 each find themselves: PASS
canary: 10903 code citations in tex/proof-guide.tex, none broken across a line: PASS

-- published-result: 0 --

-- load-bearing: 0 --

-- uncertain: 0 --

-- safe-to-delete: 2 --
  IsingModel.pseudoMassFromParamsAtPair_J_zero_h_zero  [theorem]  IsingModel/PseudoMass/FromParamsBasic/BasicSlices.lean:105
      reason: no reference outside the delete set, no citation in the scanned documentation (README.md, docs/**/*.md, tex/proof-guide.tex)
  IsingModel.pseudoMassFromParamsAtPair_J_zero_h_zero_any_pair  [theorem]  IsingModel/PseudoMass/FromParamsHZero/JZeroValues.lean:61
      reason: no reference outside the delete set, no citation in the scanned documentation (README.md, docs/**/*.md, tex/proof-guide.tex)

-- cascade (informational, never auto-deleted): 2 --
  depth 1: IsingModel.pseudoMassFromParamsAtPair_at_J_zero_h_zero_eq_zero (IsingModel/PseudoMass/FromParamsBasic/MonotonicityBounds.lean:91)
  depth 1: IsingModel.pseudoMassFromParamsAtPair_diag_h_zero (IsingModel/PseudoMass/FromParamsBasic/BasicSlices.lean:146)

-- coverage warnings: 0 (each forces `uncertain` on every candidate it could be citing) --

elapsed: 40.7s

LIMITS: this scan is textual. It cannot see simp/aesop set usage, tactic-generated
references, open/export-shortened names, or metaprogrammed names. It does not check
autoImplicit binder drift (a `#check @` dump is a separate gate). Doc rows that depend
on a lemma without naming it are invisible. Run with --lean on a green build to
cross-check the elaborated dependency graph; run --explain for the full table.
A "safe-to-delete" verdict is a necessary, not a sufficient, condition for deletion.

The cascade list above is why the BasicSlices copy is chosen for deletion: those two helpers are reachable only through _any_pair, so the hub is retained. Post-deletion scan of the two helpers reports them load-bearing (referenced by the surviving _any_pair), i.e. cascade = 0, zero new reference-0 declarations.

Verification

• Full scanner output with LIMITS: banner pasted (textual scan + --lean cross-check); both classify safe-to-delete
• Deleted name pseudoMassFromParamsAtPair_J_zero_h_zero absent repo-wide (IsingModel/docs/tex/README)
• Post-deletion scanner: two helpers load-bearing, cascade = 0 (no new reference-0 decl)
• Surviving _any_pair #check @ dump unchanged and #print axioms = [propext, Classical.choice, Quot.sound] unchanged (before/after deletion)
• lake build error-free / warning-free
• scripts/audit_gate.py --full V1-V4 PASS
• audit_gate.py --self-test (166 OK) and dead_candidate_scan.py --self-test (79 OK)
• lake exe GKSTest PASS
• Declaration-name-set diff vs main = exactly 1 deletion, 0 additions (only BasicSlices.lean changed)

🤖 Generated with Claude Code

[phasetr]

dev-issue-manager resolution verification — PASS

Independently re-verified (not just re-reading the PR body):

• CI on HEAD 69f2df3d: green (build job, run 29893716617, conclusion=success).
• Declaration diff vs base 295d8233: exactly 1 deletion (pseudoMassFromParamsAtPair_J_zero_h_zero), 0 additions, only IsingModel/PseudoMass/FromParamsBasic/BasicSlices.lean touched — confirmed via git diff --stat/git diff.
• grep -rn for the deleted name across IsingModel/ docs/ tex/ README.md: zero hits. The surviving pseudoMassFromParamsAtPair_J_zero_h_zero_any_pair remains at JZeroValues.lean:61.
• Cascade check reproduced independently: pseudoMassFromParamsAtPair_diag_h_zero and pseudoMassFromParamsAtPair_at_J_zero_h_zero_eq_zero are each referenced only by _any_pair — both load-bearing, cascade = 0, as claimed.
• Fix dead-sweep candidate extraction to require internal-dependency + docs/tex citation checks (10/22 false positives found in Profile.lean audit) #4639 adoption-rule 4th operationalization confirmed by history: refactor: drop three duplicated Lee-Yang subdomain declarations #4648 (merged), refactor: drop five unreferenced Lee-Yang convenience lemmas #4651 (merged), refactor: drop seven unreferenced bundle and Lee-Yang twin lemmas #4655 (merged), this PR refactor: drop a duplicated pseudoMassFromParamsAtPair J=0 h=0 lemma #4657 = 4th. Rule content (full scanner output + LIMITS: banner + textual/--lean + post-deletion cascade re-check) is present in the PR body, matching the refactor: drop seven unreferenced bundle and Lee-Yang twin lemmas #4655-era reinforcement (full cascade breakdown, not just a summary). No _ferromagnetic-style fixture applies to this deletion, so its absence from the checklist evidence is correct, not an omission.

Governance sync: tracking issue #4658, this PR, and the local mirror .self-local/issues/4658.md are consistent; no drift found against #4655/#4656/#4639 (all closed/merged appropriately) from this /goal session.

Verdict: resolved, PR is mergeable, tracking issue #4658 may be closed on merge.