Pith. sign in
module module moderate

IndisputableMonolith.QFT.RS_QFT_Structural_004

show as:
view Lean formalization →

Structural certificate module for RS-QFT item 004: a nonnegative domain cost functional together with a strictly positive canonical threshold. Anyone wiring QFT sector bounds to the RS cost layer cites this pack. The module is mostly definitions plus elementary nonnegativity and positivity lemmas, closed by an inhabited certificate record.

claimThe module introduces a domain cost $C_{\mathrm{dom}}$ (nonnegative), a canonical threshold $\theta_{\mathrm{can}}>0$, and a certificate record asserting these structural facts for RS-QFT item 004.

background

Recognition Science routes continuum and field-theoretic structure through the same cost layer used for the discrete forcing chain. The imported Cost module supplies the J-cost infrastructure ($J(x)=(x+x^{-1})/2-1$), while Constants fixes the RS-native tick. In the QFT sector one still needs a domain-level cost that stays nonnegative and a positive threshold against which structural inequalities can be stated.

This module packages those two ingredients for structural claim 004: a domain cost functional and a canonical threshold, with the elementary sign facts needed before any dynamical or spectral argument. No continuum limit or renormalization step is taken here; the objects are pure structural scaffolding for later QFT certificates.

proof idea

Definition-first module. domainCost and canonicalThreshold are introduced as defs; domainCost_nonneg and canonicalThreshold_pos are short nonnegativity/positivity lemmas (typically unfolding and applying Cost-layer facts). domainCost_at_eq records an evaluation identity. RSQFTStructural004Cert bundles the properties into a certificate type; cert and cert_inhabited supply a concrete inhabitant so downstream code can assume the pack is available.

why it matters in Recognition Science

Gives the QFT side a named, certifiable handle on domain cost and threshold structure before heavier analytic work. Downstream used-by edges are empty in the current graph, so this is a leaf certificate pack rather than a lemma feeding a named parent theorem. It sits in the QFT domain of the monolith and aligns with the broader program of discharging RS structural obligations as inhabited certificate records rather than free-floating axioms. Landmarks touched only indirectly: the Cost import ties back to J-uniqueness (T5) and the RCL, but this file does not reprove those.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)