Internal adjudication (IIb/PT layer) is reinterpreted as decoding/repair of semantic inconsistency in distributed records. We formalize record fragments as codeword-like constraints and a uniform decoder-claim predicate on encoded instances. Under the SelectorStrength barrier schema (Paper 29), no total-effective decider exists for this predicate over encoded instances when anti-decider closure and a fixed-point premise hold. Stratified decoding is possible; societies improve decoding coverage, and diversity is necessary for strict improvement (Paper 40). A minimal toy (two instance types: consistent / ambiguous) witnesses nontriviality; the barrier applies under the usual strength premises. The development is mechanized in Lean 4 as the ErrorCorrectingClosure library in nems-lean, with zero sorry and no custom axioms. Trust boundary. Decoder-claim barriers assume the Paper 29 package on the encoded domain; stratified decoding and institutional coverage improvements carry their own hypotheses (Paper 40). Mechanization is nems-lean . See .
Nova Spivack (Sun,) studied this question.