ShannonFalsifier
plain-language theorem explainer
ShannonFalsifier is a record type that holds candidate counterexamples to equating Shannon entropy with expected J-cost over probability distributions. Information theorists and Recognition Science workers cite it when checking the empirical reach of the J-cost derivation. The definition consists of two string fields, one naming the falsifier and one recording its status.
Claim. A record type whose instances pair a string description of a potential falsifier with a string status, where the falsifiers are compression below entropy, communication above capacity, or mismatch between thermodynamic and information entropy.
background
The Information.ShannonEntropy module derives Shannon entropy H = -Σ p_i log(p_i) from J-cost minimization, with J(x) = (x + x^{-1})/2 - 1. Probability distributions carry information cost via deviation from uniformity; total J-cost minimization recovers the entropy expression. Upstream structures supply the J-cost definition (PhiForcingDerived.of) and its convexity (PhysicsComplexityStructure.of), while RSNativeUnits.status fixes the native units with ħ = φ^{-5}.
proof idea
This is a structure definition that introduces the falsifier record type with no computational body. Field accessors are generated automatically from the two string components.
why it matters
The structure supplies the type used by experimentalStatus to enumerate verified cases, thereby supporting the module target of deriving Shannon entropy from J-cost. It interfaces with the broader forcing chain through the convexity and local dynamics of J, and with the paper proposition INFO-001 on information theory foundations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.