Discharge matrix exp-log normalization hardbone leaf

[freezed-corpse-143]

Summary

• Proves the local hardbone CFC normalization leaf matrixExpLogSelfAdjointNormalization for self-adjoint matrix exponentials.
• Exposes the theorem through hardbone API, judge, and example checks.
• Updates RandomMatrix docs/status to mark only this pointwise normalization leaf complete while preserving the remaining Tropp/Lieb, integrability, variance-proxy, rank/effective-rank, and Matrix Bernstein non-goals.

Motivation

This discharges the smallest theorem-backed hardbone leaf selected after the RM-HB12 audit: CFC.log (matrixExp A) = A for self-adjoint A, using Mathlib's CFC.log_exp and the repository's matrixExp wrapper.

Scope

• Adds one local theorem witness for an existing statement target.
• Adds API/judge/example availability checks.
• Updates docs only to reflect this narrow proof leaf.
• Does not prove Lieb/Jensen, Golden-Thompson, trace-exp integrability propagation, variance-proxy control, rank/effective-rank refinements, full Matrix Bernstein, or unconditional sample-covariance concentration.

Testing

• RED: lake env lean HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean failed on missing matrixExpLogSelfAdjointNormalization before implementation
• git diff --check upstream/main...HEAD
• lake build HighDimProb.RandomMatrix.HardboneStatements
• lake env lean HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean
• lake env lean HighDimProbJudge/RandomMatrix/TraceExpUse.lean
• lake env lean HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean
• python scripts/judge_policy_check.py
• python .github/scripts/check_text_quality.py
• lake build HighDimProbJudge
• lake build HighDimProb.Examples
• lake test
• lake build

Pre-PR hygiene

• Base/head skew after fetch: upstream/main...HEAD = 0 1
• Merge-tree preflight: clean