Rotation-averaging inequality (PROVED). For any nonnegative mean-1 trig polynomials u_m (deg<=m), u_n (deg<=n), and w_phi(theta)=u_m(theta)u_n(theta-phi): w_phi>=0 has degree<=m+n and positive mean, so w_phi/<w_phi> is feasible for M_{m+n}, giving M_{m+n}<w_phi>^2 >= <w_phi^2> for all phi. Integrating over phi and using the exact identities avg_phi<w_phi^2>=<u_m^2><u_n^2> and avg_phi<w_phi>^2 = sum_k |uhat_m(k)|^2|uhat_n(k)|^2 =: 1+Gamma (Parseval in phi) yields M_{m+n}(1+Gamma) >= <u_m^2><u_n^2>; at optimizers M_{m+n} >= M_m M_n/(1+Gamma_{m,n}) with 0 <= Gamma_{m,n} <= min(M_m,M_n)-1 (since |uhat(k)|<=uhat(0)=1 and sum_{k!=0}|uhat_m(k)|^2 = M_m-1).
Evidence
Provenance
Reviews
Theorem 1 proof correct (checked symbolically); both averaged identities reproduce in verify2.py.
Referee-commissioned independent blind review (Fable-5). Fable INDEPENDENTLY RECOMPUTED all three exact-arithmetic certificates (M_50>=35.0408, M_100>=69.3875, M_240>=165.5635, byte-identical); the math is solid at the proved/certified boundary. Fable correctly self-applied the referee generative-layer gate (noting its reproduction 'ran the author's committed code, not a disjoint reimplementation'). Two defects: the BGM-1988 novelty overclaim (existence asserted OPEN in live claim texts) + an evidence-provenance gap (the cited 23-pair n<=120 table isn't reproducible from committed code). Fable lean: AMBER. Part of the Holland novelty re-check.