Pith. sign in
module module moderate

IndisputableMonolith.QFT.RS_QFT_Structural_002

show as:
view Lean formalization →

Structural QFT layer that packages a domain-level cost functional, its nonnegativity and evaluation identities, and a positive canonical threshold into an inhabited certificate. QFT workers cite it when they need a single RS-native cost gate rather than raw J-cost. The module is mostly definitional: identities reduce by unfolding, positivity follows from the Cost import.

claimA domain cost $C(\Omega)$ built from the RS $J$-cost, with $C(\Omega)\ge 0$ and a canonical threshold $\theta>0$, packaged as an inhabited structural certificate for RS-QFT.

background

Recognition Science measures mismatch by the unique cost $J(x)=(x+x^{-1})/2-1$ fixed by the Recognition Composition Law. The Cost import supplies that functional and its elementary inequalities; Constants supplies the RS time quantum $\tau_0=1$ tick used to normalize discrete QFT domains.

This module lifts pointwise $J$ to a domain-level cost $C(\Omega)$ on structural regions of the QFT side, then isolates a single positive scale $\theta$ (the canonical threshold) against which domain costs are compared. Sibling declarations record evaluation at equality cases, nonnegativity of $C$, and positivity of $\theta$.

The certificate bundle RSQFTStructural002Cert is the export surface: downstream QFT lemmas can assume one inhabited cert rather than re-proving the cost and threshold facts separately.

proof idea

Definition module with thin supporting lemmas. domainCost and canonicalThreshold are introduced by definition from Cost and Constants. domainCost_at_eq is an unfolding identity. domainCost_nonneg and canonicalThreshold_pos inherit nonnegativity and positivity from the upstream Cost facts. The certificate record is assembled by packing those fields; cert_inhabited is a one-line constructor application showing the record is nonempty.

why it matters in Recognition Science

Gives the QFT sector a single structural cost-and-threshold certificate instead of ad-hoc appeals to raw $J$. In the RS forcing chain this sits downstream of T5 ($J$-uniqueness) and the Cost library, and upstream of any domain-gate or structural-stability arguments that need $C(\Omega)\ge 0$ and a fixed positive cutoff $\theta$. No downstream consumers are wired in the graph yet; the module is an export stub for later RS-QFT structural theorems that will cite the inhabited cert rather than rebuild the cost layer.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)