Pith. sign in
module module moderate

IndisputableMonolith.Foundation.LambdaQCD_RS_v3

show as:
view Lean formalization →

Module packaging the Recognition Science (v3) account of the QCD scale Λ_QCD. It defines a domain cost on the relevant RS sector, a positive canonical threshold, and an inhabitation certificate that the forced scale sits at that threshold. Cite it when wiring Λ_QCD into the RS constant ladder or when checking nonnegativity and positivity lemmas for the cost. Structure is definitional plus short positivity/equality lemmas and a cert record.

claimOn the RS cost sector for QCD, a domain cost $C$ is defined with $C\ge 0$ and an equality form at the evaluation point; a canonical threshold $\theta>0$ is fixed; and a certificate record asserts that the RS-native $\Lambda_{\mathrm{QCD}}$ is realized at that threshold (v3 packaging).

background

Recognition Science forces dimensionless structure from the J-cost $J(x)=(x+x^{-1})/2-1$ (T5) and the golden ratio $\varphi$ as self-similar fixed point (T6), with dimensionful anchors set in RS-native units ($c=1$, $\hbar=\varphi^{-5}$, etc.). The Cost import supplies that cost language; Constants supplies the tick quantum $\tau_0=1$.

This module specializes that machinery to the QCD scale. Sibling definitions introduce a domain cost on the QCD sector, prove it is nonnegative, and record an equality identity at the evaluation point used by the certificate. A separate canonical threshold is fixed and shown positive. The certificate bundle (LambdaQCD_RS_v3Cert / cert) packages the claim that the RS-forced $\Lambda_{\mathrm{QCD}}$ sits at that threshold.

The local setting is Foundation: close the constant ladder entry for $\Lambda_{\mathrm{QCD}}$ without reopening the T0–T8 forcing chain.

proof idea

Definition module with thin lemma layer, not a deep derivation. Domain cost is introduced by definition; nonnegativity and the on-point equality are short algebraic or unfolding lemmas over the Cost API. Canonical threshold is a positive constant (positivity lemma). The certificate is an inhabited structure packing those facts into a single v3 claim object. No multi-step tactic proof of a new physical identity appears at module scope; the work is packaging and sign/equality hygiene.

why it matters in Recognition Science

Gives the Foundation a named, certifiable handle on $\Lambda_{\mathrm{QCD}}$ in RS units so downstream constant and mass-ladder work can cite one object rather than ad hoc cost evaluations. It sits on Constants and Cost and does not itself appear as a used-by parent in the current graph, so its role is supply-side: feed any later theorem that needs a nonnegative domain cost, a positive threshold, or an inhabited $\Lambda_{\mathrm{QCD}}$ certificate. Landmark contact is indirect: J-uniqueness (T5), $\varphi$ (T6), and the RS unit conventions that place strong-sector scales on the $\varphi$-ladder. Does not reopen spatial dimension (T8) or the eight-tick octave (T7).

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)