pith. sign in
module module moderate

IndisputableMonolith.Physics.QuantumTunnelingFromJCost

show as:
view Lean formalization →

This module applies the canonical J-cost band template to derive quantum tunneling regimes and certificates in Recognition Science. Physicists seeking a J-cost foundation for tunneling effects would cite it when building domain certs. The structure consists of regime definitions and a certification object built directly on the imported six-clause template from CanonicalJBand.

claimThe module introduces $TunnelingRegime$ as the set of positive ratios satisfying the J-cost band conditions for tunneling and $QuantumTunnelingCert$ as the six-clause certificate that tunneling occurs whenever the J-cost on the ratio meets the matched-zero and nonnegativity clauses.

background

The upstream CanonicalJBand module supplies the reusable six-clause J-cost-on-ratio template used across master cert chains. It establishes that J(1) = 0 and J(x) ≥ 0 for all x > 0, with J defined via the Recognition Science functional equation as J(x) = (x + x^{-1})/2 - 1. This module sits in the physics domain and imports that template to specialize the band for tunneling.

proof idea

This is a definition module, no proofs. It organizes the argument by declaring TunnelingRegime and QuantumTunnelingCert as direct applications of the six-clause template imported from CanonicalJBand, together with counting and certification helpers.

why it matters in Recognition Science

The module supplies one of the B-tier physics domain certs in the master chain, extending the J-cost framework to quantum tunneling. It feeds downstream quantum mechanics derivations that rely on the same band template for other effects such as the alpha band and mass ladder.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)