feat(space): add half-plane surface

[Robby955]

Summary

Adds the half-plane surface API under PhyslibAlpha.SpaceAndTime.Space.Surfaces.

Changes

• Defines halfPlaneDomain as the nonnegative coordinate half-plane inside Space 2.
• Defines halfPlane : Space 2 → Space 3 as the coordinate-plane embedding through slice 2.
• Adds injectivity, continuity, measurable embedding, and norm lemmas.
• Adds the induced half-plane surface measure by restricting Space 2 volume to halfPlaneDomain before mapping into Space 3.
• Adds tempered-growth and SFinite instances for halfPlaneMeasure.
• Adds the corresponding distribution and integral application lemmas.
• Proves the half-plane image has ambient Space 3 volume zero, by containment in a proper coordinate submodule.

[github-actions]

Thank you for this PR, which will now be reviewed.
If submitting to ./Physlib or ./QuantumInfo, 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 are submitting to ./PhyslibAlpha there will be a lighter review process,
though your PR must still pass the automated checks.

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

[jstoobysmith]

Looks good to me - many thanks for all these PRS :).