SourceDominantBlend.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The dominant branch of the actual source comparison. Raw amplitude motion and complementary-mass coefficient motion feed the proved logarithmic comparison; the residual error is absorbed by the prescribed blend.

theorem OAI.LipschitzHilbert.source_dominant_prediction_comparison line 16