[dcl.contract.func]/4 says
A declaration D of a function or function template f that is not a first declaration shall have either no function-contract-specifier-seq or the same function-contract-specifier-seq (see below) as any first declaration F reachable from D.
If D and F are in different translation units, a diagnostic is required only if D is attached to a named module.
If a declaration F₁ is a first declaration of f in one translation unit and a declaration F₂ is a first declaration of f in another translation unit, F₁ and F₂ shall specify the same function-contract-specifier-seq, no diagnostic required ([ifndr:dcl.contract.func.mismatched.contract.specifiers]).
There are two IFNDR cases, one about not-the-first declarations and another is about first declarations.
However, G.6.4 is only about the latter case.
If two different first declarations of a function (which must therefore not be reachable from one another) do not have equivalent function contract specifiers the program is ill-formed, no diagnostic required.
BTW, [dcl.contract.func]/5 has a totally missing IFNDR
... If this condition is not met solely due to the comparison of two lambda-expressions that are contained within P₁ and P₂, no diagnostic is required.
[dcl.contract.func]/4 says
There are two IFNDR cases, one about not-the-first declarations and another is about first declarations.
However, G.6.4 is only about the latter case.
BTW, [dcl.contract.func]/5 has a totally missing IFNDR