Pith. sign in
module module moderate

IndisputableMonolith.Information.Information

show as:
view Lean formalization →

Module packaging domain-level information cost, a canonical positive threshold, and certificate scaffolding for capacity bounds in Recognition Science. Cite it when lifting the scalar J-cost to domain measures or when wiring Q-capacity certificates. Structure is mostly definitions plus elementary nonnegativity and positivity lemmas over the imported Cost and Constants layers.

claimIntroduces a domain cost $C$ built from the RS cost $J$, proves $C \ge 0$ and evaluation identities, fixes a canonical threshold $T > 0$, and exposes certificate types (including a depth-4 Q-capacity certificate) with an inhabited instance.

background

Recognition Science measures mismatch by the unique cost $J(x) = (x + x^{-1})/2 - 1$ forced by the Recognition Composition Law. The Cost import supplies that scalar $J$; Constants supplies the RS-native tick $\tau_0 = 1$.

This module lifts those primitives to an information layer: a domain cost that aggregates $J$-type mismatch over a domain, a canonical numerical threshold used as a cut for certificates, and certificate objects that package capacity claims (notably a depth-4 Q-capacity certificate). Sibling lemmas record that the domain cost is nonnegative and that the threshold is strictly positive.

The setting is definitional infrastructure for later information and capacity arguments, not a forcing-chain step (T0–T8) by itself.

proof idea

Definition-heavy module. Domain cost is introduced and tied to evaluation identities; nonnegativity follows from the corresponding property of $J$. The canonical threshold is defined and shown positive by a direct positivity argument. Certificate types (including QCap4DeepCert) are declared with an inhabited instance so downstream code can inhabit the cert interface without new analytic work here.

why it matters in Recognition Science

Gives the information-domain vocabulary that later RS capacity and certification arguments can import: domain cost, threshold, and cert shells. No downstream used_by edges are recorded on this page yet, so it currently sits as a leaf infrastructure module under the Information domain rather than a named parent theorem. It does not itself force $\phi$, the eight-tick octave, or $D=3$; those remain upstream in the forcing chain. Its role is to keep cost-to-information bookkeeping and certificate hooks in one place.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)