QuantumTunnelingCert
plain-language theorem explainer
Physicists modeling tunneling amplitudes via J-cost cite this certificate to confirm exactly five regimes and to anchor the classical-to-quantum transition at the canonical J-band. The five regimes are classical forbidden, thermally assisted, direct tunneling, resonant tunneling, and over-barrier, matching the configuration dimension D=5. The structure is assembled as a direct definition that bundles the Fintype cardinality fact with the six-clause CanonicalCert.
Claim. A structure certifying that the set of tunneling regimes has cardinality five and that the transition threshold is given by the canonical certificate satisfying $J(1)=0$, $J(x)=J(1/x)$ for $x≠0$, $J(φ)>0$, $0.11<J(φ)<0.13$, and $J(1/φ^2)>0$.
background
Recognition Science models the tunneling amplitude as the J-cost of the momentum-to-barrier ratio, with rate $T∝exp(-2κd)$. The module introduces five regimes via the inductive type whose constructors are classical forbidden, thermally assisted, direct tunneling, resonant tunneling, and over-barrier; these are declared to derive Fintype so that their count equals the configuration dimension D=5. The transition to classically allowed transmission is marked when the J-cost crosses the canonical band $J(φ)∈(0.11,0.13)$ in RS-native units where $c=1$ and $ℏ=φ^{-5}$.
proof idea
The declaration is a plain structure definition. It obtains the cardinality equality from the Fintype instance derived on the five-constructor inductive type and imports the CanonicalCert structure directly from the CanonicalJBand module.
why it matters
The structure is instantiated by the downstream quantumTunnelingCert definition and supplies the regime count and transition threshold required for the tunneling module. It records the link between the five-regime classification and configDim D=5 while anchoring the threshold at the phi-band from the T5 J-uniqueness and phi fixed-point steps of the forcing chain. The construction thereby connects the tunneling model to the Recognition Composition Law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.