Pith. sign in
module module moderate

IndisputableMonolith.Information.CompressionPrior

show as:
view Lean formalization →

The CompressionPrior module shows that the golden-ratio prior is the unique minimum-description-length prior forced by J-cost uniqueness (T5). Information theorists and RS auditors cite it to ground MDL coding lengths in the recognition cost. The argument reduces MDL uniqueness to the already-proved uniqueness of J from the Cost layer.

claimThe $\varphi$-prior is the unique minimum description length (MDL) prior induced by the J-cost $J(x)=(x+x^{-1})/2-1$, as forced by T5 J-uniqueness. Sibling objects package the prior, a coding-length functional, and the assertion that the prior holds.

background

Recognition Science derives physics from a single cost functional. T5 of the forcing chain establishes uniqueness of the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). This module lives in the Information domain and imports the Cost layer so that uniqueness of $J$ can be read as uniqueness of an MDL prior.

Minimum Description Length selects the hypothesis that minimizes total description length of model plus data. Here coding length is measured by J-cost, so the prior over hypotheses is forced rather than chosen by hand. The module exposes three sibling objects: the MDL prior construction, a coding-length map, and a predicate that the $\varphi$-prior holds.

The parent Information aggregator collects this module with the EML-from-recognition bridge as the information-theoretic foundation of RS.

proof idea

The module is organized around three siblings: an MDL prior construction, a coding-length functional, and a theorem that the $\varphi$-prior holds uniquely. Uniqueness is inherited from T5 J-uniqueness in the Cost import: once $J$ is the unique admissible cost, the induced MDL prior is uniquely $\varphi$-weighted. The development is definitional packaging plus a uniqueness claim, not a long independent tactic proof.

why it matters in Recognition Science

Downstream, IndisputableMonolith.Information imports this module as the MDL half of the information bridge, described there as "Minimum Description Length (MDL) grounded in J-cost." It supplies any later result that needs a canonical prior on the $\varphi$-ladder or a forced coding length. In the forcing chain it closes the link from T5 J-uniqueness to an operational compression prior, complementary to the oriented exp-log compiler gate in the sibling EML module. Without it, RS would lack a unique information prior tied directly to the recognition cost.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)