Pith. sign in
module module moderate

IndisputableMonolith.Foundation.RS_FDN_Structural_003

show as:
view Lean formalization →

Foundation module packaging the domain-cost functional and its canonical positive threshold used by structural certificate RS-FDN-003. It records nonnegativity of the cost, evaluation at equality, and an inhabited certificate bundle. Anyone citing the structural forcing chain or cost-threshold gates would import it. The file is mostly definitions plus short positivity and equality lemmas over the Cost layer.

claimDefine a domain cost $C$ (built from the RS $J$-cost), prove $C \ge 0$ and the on-equality evaluation identity, fix a canonical threshold $\theta > 0$, and package these facts as an inhabited structural certificate for RS-FDN-003.

background

Recognition Science measures mismatch with the $J$-cost from the Cost module, $J(x)=(x+x^{-1})/2-1$, which is nonnegative and vanishes only at $x=1$. Constants supplies the RS-native tick $\tau_0=1$. This module lifts that cost to a domain-level functional (domain cost) and fixes a single positive canonical threshold against which structural claims are checked.

The local setting is the Foundation structural series: short, certificate-shaped modules that pin elementary analytic facts (nonnegativity, positivity of a threshold, evaluation identities) so later forcing or ledger arguments can cite one named bundle rather than reopen the Cost API.

Upstream material is thin: only Constants and Cost are imported. No deeper forcing-chain theorems are required here; the module stays at the level of cost calculus and a threshold constant.

proof idea

Definition-heavy module. Domain cost is introduced as a thin wrapper around the Cost layer; equality-at-matching and nonnegativity are short lemmas reducing to the corresponding $J$-cost facts. The canonical threshold is a positive constant (positivity proved by a direct numeric or algebraic check). The certificate record simply bundles these fields; inhabitation is by constructing that record from the lemmas above. No multi-step tactic developments.

why it matters in Recognition Science

Gives the Foundation layer a named structural certificate (RS-FDN-003) for domain cost and its threshold, so later recognition or ledger arguments can depend on one inhabited bundle instead of ad-hoc Cost lemmas. Downstream use is not yet wired in this graph (no used_by edges), but the sibling certificate pattern matches other RS-FDN structural pins that feed forcing and measurement gates. Ties to the cost side of the framework (J-uniqueness / T5 background) without claiming any step of the T0–T8 chain itself. Closes a small scaffolding slot: threshold positivity and cost nonnegativity are discharged here rather than left sorry'd upstream.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)