Pith. sign in
module module moderate

IndisputableMonolith.Foundation.RecognitionSpectrum3_FromJCost

show as:
view Lean formalization →

Foundation module that builds a three-mode recognition spectrum from the J-cost: a domain cost, its nonnegativity, a positive canonical threshold, and an inhabited certificate RecogSpectrum3Cert. Foundation authors cite it when tying J-uniqueness to the forced three-dimensional recognition band. The file is mostly definitions and elementary positivity lemmas closed by a certificate inhabitation.

claimFrom the J-cost one obtains a domain cost $C$ on the recognition domain, with $C\ge 0$, a canonical threshold $\theta>0$, and an inhabited certificate that the three-mode recognition spectrum is realized by this cost data.

background

Recognition Science forces the unique symmetric cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) via the Recognition Composition Law and the T5 uniqueness step. The present module sits in the Foundation layer and imports the RS constants (including the native tick) together with the Cost library that supplies $J$ and related cost primitives.

The local objects are a domain-level cost assembled from $J$, equality and nonnegativity facts for that cost, and a canonical positive threshold used to cut the spectrum. The certificate type packages these pieces into a single witness that a three-mode recognition spectrum arises from the J-cost data, matching the $D=3$ landmark in the forcing chain.

proof idea

Definition-heavy module rather than a deep proof development. It introduces the domain cost and proves pointwise equality and nonnegativity by reduction to the underlying J-cost properties from the Cost import. The canonical threshold is defined and shown positive by a direct positivity argument. The certificate structure is then assembled and inhabited, yielding a concrete witness that the three-mode spectrum data is available from J.

why it matters in Recognition Science

Closes a Foundation packaging step: the unique J-cost (T5) is turned into explicit three-mode spectrum data aligned with the forced spatial dimension $D=3$ (T8). Downstream pages can consume the inhabited certificate instead of rebuilding domain cost and threshold lemmas. No further used-by edges are recorded on this page yet; the module is the hand-off point from pure cost theory into spectrum certificates used by later recognition and forcing arguments.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)