Record Entropy and Noncomputability: Monotone Semantic Complexity under Diagonal Capability Paper 42 of the NEMS Suite

Paper 41 introduced the refinement flow of world-types: as records accumulate, stage equivalence refines and forgetful maps form a coherent, natural system. This paper defines record entropy \\entropy(t) as the cardinality of stage world-types at time t—a purely semantic measure of record complexity. We prove that \\entropy(t) is monotone under record growth (\\entropy(t+1) \\ge \\entropy(t)) and strict when refinement is strict. We then establish a uniform entropy decision barrier: no total-effective decider exists for a uniform entropy-claim predicate over encoded filtrations/times, under anti-decider closure and fixed-point premise (same DiagCap/hFP as Papers 29–30). A toy witness (two-bit filtration) exhibits monotonicity and strict growth at t=0; the barrier concerns uniform decision over encoded instances. The development is mechanized in Lean 4 as the RecordEntropy library in nems-lean, with zero sorry and no custom axioms. Trust boundary. The uniform entropy decision barrier is indexed by anti-decider closure and hFP on encoded instances; monotonicity/strict-growth lemmas are conditional on the filtration model. Mechanization is nems-lean . See .