docs: replace declaration provenance with semantic references

[phasetr]

Closes #5019
Closes #5026

Intent

Finish the unresolved provenance portions of both errata issues. Declaration documentation should
describe the current theorem and its semantic dependencies; workflow step numbers, issue IDs and
PR numbers belong in Git history and become opaque as the implementation evolves.

Changes

• Remove the 26 remaining PR #N, bare #N, and Step N references from declaration docs in
  AmbientLattice/Analyticity*.lean (the live-main population after docs(errata): PR1 of 2 — false-claim corrections from #4984 campaign errata #5030).
• Replace provenance in the originally reported AmbientLatticeSum files with actual dependency
  names such as freeEnergyAlongExhaustion_le_uniform_upper_bound,
  freeEnergyInfinite_high_temp_h_zero_deviation_bound_exp, and
  log_partitionFunction_sum.
• Extend the same bounded cleanup to the adjacent InducedUnion.lean and
  PerStageIncrement.lean files found by the required live boundary sweep. These carried the same
  issue/PR-number defect class and are direct dependencies of the reported layer.
• Address E4 from issue Errata: pre-existing /-- doc-comment defects in the AmbientLatticeSum layer (found in wave 15 of #4984) #5026 in SuperadditiveConvergence.lean: remove the embedded progress transition and
  replace the obsolete future-PR roadmap with the current of_J_zero / of_beta_zero constructors
  plus the general direct-field route.
• Preserve GJ section/theorem attribution and all mathematical explanations; no Lean term,
  declaration signature, import, or dependency changed.

History and scope evidence

• git log -S and blame show the Analyticity prose was carried through file splits such as
  922a5b2c, while the AmbientLatticeSum prose was carried through 01e6f84b/1002f3a3.
• A live-main search found 26 Analyticity occurrences rather than the issue's original 31 because
  docs(errata): PR1 of 2 — false-claim corrections from #4984 campaign errata #5030 had already rewritten part of that population.
• The final bounded scan over AmbientLattice/Analyticity*.lean, AmbientLatticeSum/, and the
  AmbientLatticeSum root modules reports zero PR #N, bare #N, Step N, or Issue #N tokens.
• The E4 progress/roadmap phrases also report zero occurrences.

Verification

• Full Nix lake build IsingModel: PASS, 4943 jobs.
• audit_gate.py --full: PASS over 1921 Lean files; all 13 capstones remain limited to the standard
  three axioms.
• Header inventory ratchet: PASS, live/baseline 150/79.
• git diff --check: PASS.
• The diff is prose-only by inspection: declarations and proof terms are unchanged.