feat(Space): add dimension wrapper for fundamental solution Laplacian

[Lemmy00]

This is a small follow-up to #1171 and to the Zulip discussion about public statements exposing d.succ.succ.succ.

The PR adds a user-facing wrapper theorem:

Space.distLaplacian_fundamentalSolution_norm_zpow_of_three_le

It states the fundamental-solution Laplacian theorem for Space d under the explicit hypothesis 3 ≤ d, with exponent 2 - d. The existing d.succ.succ.succ theorem remains the implementation lemma, so this does not attempt a broader API refactor.

Verification:

• lake env lean Physlib/SpaceAndTime/Space/Norm.lean
• lake build Physlib.SpaceAndTime.Space.Norm
• lake build Physlib
• lake exe runPhyslibLinters
• ./scripts/lint-style.py Physlib/SpaceAndTime/Space/Norm.lean
• git diff --check

[github-actions]

Thank you for this PR, which will now be reviewed. Please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.