Pith. sign in
module module moderate

IndisputableMonolith.Foundation.RS_Quantum_Tunneling_Rate

show as:
view Lean formalization →

Defines the Recognition Science quantum tunneling rate from a nonnegative domain cost functional and a positive canonical threshold. Supplies an inhabited certificate bundle packaging the cost identities and threshold positivity. Cited by anyone wiring RS barrier penetration into mass or decay estimates. The module is definitional scaffolding plus elementary nonnegativity and positivity lemmas.

claimIntroduce a domain cost $C$ on the RS configuration space, prove $C \ge 0$ and an evaluation identity at equality cases, fix a canonical threshold $\theta > 0$, and package these into an inhabited RS quantum-tunneling certificate.

background

Recognition Science treats barrier penetration as a cost-crossing event on the $\phi$-ladder rather than a WKB integral in continuum QM. The cost side of the story lives in Cost (the $J$-cost $J(x)=(x+x^{-1})/2-1$ and its composition law). Constants supplies the RS tick $\tau_0=1$ against which rates are later normalized.

This module localizes that cost to a "domain" (the classically forbidden region in RS units) and names a single positive threshold that the cost must exceed for a tunneling event to register. The certificate type is the standard RS pattern: a structure bundling the numeric witnesses so downstream modules can assume one inhabited instance rather than re-proving positivity.

proof idea

Definition module with thin lemmas. domainCost is introduced as a real-valued functional; domainCost_at_eq and domainCost_nonneg discharge the evaluation identity and nonnegativity by direct appeal to the imported cost axioms. canonicalThreshold is a positive real constant; positivity is a one-line arithmetic fact. RSQuantumTunnelingCert packages the above; cert and cert_inhabited exhibit a concrete inhabitant. No deep tactic proof; the work is naming and packaging.

why it matters in Recognition Science

Gives the Foundation layer a named tunneling-rate interface so mass-ladder and decay modules can cite a single certificate rather than ad-hoc cost inequalities. Sits downstream of the $J$-uniqueness forcing step (T5) and the cost module, and upstream of any rate or width calculation that needs a barrier threshold in RS-native units. No external used-by edges are recorded yet; the module is the attachment point for those edges. Touches the Berry-scale creation threshold only by analogy (both are positive cost cutoffs); it does not derive $\phi^{-1}$ here.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)