Information Shannon Entropy Max Rs Shannon Entropy Max Cert

The certificate's actual scope

Shannon entropy measures the average information content of a message, and for a set of n equally likely symbols the maximum entropy is H_max = log2(n) bits. The Recognition Science declaration ShannonEntropyMaxCert appears, by name and by its accompanying research note, to aim at a claim about this maximum: at an alphabet size of n = phi^k, where phi is the golden ratio, the maximum entropy would be k * log2(phi) = k * 0.694 bits, and recognition systems at such an alphabet would maximize information efficiency.

What the declaration actually establishes is narrower and different. The machine-checked library of formal theorems proves three facts about a function called domainCost, defined as Jcost(m/e) where Jcost(x) = (x + 1/x)/2 - 1. First, when m equals e and both are nonzero, domainCost equals zero. Second, for positive m and e, domainCost is nonnegative. Third, the quantity phi - 3/2 is positive. The certificate ShannonEntropyMaxCert packages these three statements together, and the library proves the certificate is inhabited, meaning such a certificate exists.

In Recognition Science, the framework models a ledger (a discrete record of events) and a cost (a forced penalty for recognition) through the function Jcost. The three proved facts are general properties of this cost function: it vanishes when its two inputs match, it never goes negative for positive inputs, and the golden ratio exceeds 1.5. These are real theorems, but they make no reference to Shannon entropy, to alphabets, to symbols, or to information efficiency. The research note in the source file says plainly that the paragraph about entropy is where the idea was meant to go, not a result.

The gap is definitional. The certificate defines domainCost as Jcost(m/e) without ever defining what m and e mean for a recognition system or for an alphabet. Without definitions of m and e in the subject's own terms, the certificate cannot be a theorem about Shannon entropy. What would make it one is a definition of m and e tied to the entropy setting. The honest summary: the declaration proves three true but generic facts about the cost function, and it does not prove the entropy-maximization claim its name suggests. The entropy claim remains a research note, not a theorem.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

theorem cert_inhabited : Nonempty ShannonEntropyMaxCert := ⟨cert⟩

What this page does not claim

The certificate does not prove that H_max = log2(n) for n symbols. The certificate does not prove that recognition systems at phi-rung alphabets maximize information efficiency. The certificate does not define m or e in terms of Shannon entropy or alphabets.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/Shannon_Entropy_Max_RS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: