CMDG-CONDENSED-CM4-P3-F-001: certify coefficient-object solidity

[fyremael]

Refs #472, #465, #464, #448, #355.

Purpose

Begin the exact P3-F execution sequence:

1. certify lowerHomEquiv;
2. certify finite-quotient lift / surjectivity;
3. isolate GLOBAL_SECTIONS_DOUBLE_INTERNAL_DUAL_SURJECTIVITY as the condensed mapping-out residue;
4. prove injectivity;
5. certify CoefficientResidualHomTheorem.

Stacked predecessor state

This draft is intentionally stacked on P3-E branch agent/cmdg-condensed-cm4-p3-e-001 at head 78c8693ecd10a33bac44ba6dfe185f8e7a3bf06d. P3-E has fresh exact-head green CI, but its fresh exact-head independent review and protected admission are still pending. Therefore this PR carries preparation/replay authority only until #465 is protected-merged and read back. It must then rebind/retarget to the admitted protected state.

Current scope

The first commit exposes the lower Hom set

((Condensed.profiniteFree R).obj X ⟶ coefficientObject)

as LocallyConstant X R through the pinned free-forgetful adjunction and GrothendieckTopology.uliftYonedaEquiv. The P3 audit imports this module so the existing pinned P3 replay kernel-checks the construction.

No coefficient solidity, CoefficientResidualHomTheorem, injectivity, P3 availability, P4/P5/P6, final CM4, derived/complex statement, arbitrary-ring generalization, or broader CMDG authority is claimed.