nx_codec_caps_gate.nx

nx_codec_caps_gate.nx -- proves the advertised header equals the capability. The property under test is an IFF, in both directions, over the whole registry: a format appears in the emitted header if and only if we can decode it. T1 walks every registry entry and checks both directions at once, so neither an over-claim (advertise what we cannot read) nor an under-claim (hide what we can) can survive. T3 and T4 pin the two live defects by name. `image/avif` and `br` were being advertised by nx_http_client and nx_polite_browser respectively with no decoder behind either. If someone flips those registry flags to 1 without landing the decoders, T1 still passes -- so T3/T4 assert the SPECIFIC absence, and they are meant to be deleted by the same commit that lands the decoder, not before. T7 is the non-vacuity control: an unknown format must answer 0, not a plausible 1. If the query answered 1 for anything it did not recognise, T1's forward direction would be satisfiable by an empty registry. license_tier: ORIGINAL