Pith. sign in
module module moderate

IndisputableMonolith.Physics.PhotoelectricEffectFromJCost

show as:
view Lean formalization →

Module derives the photoelectric threshold from the J-cost: emission begins exactly when J(W/hν)=0, i.e. when photon energy equals the work function. Supplies material data, the threshold predicate, a below-threshold no-emission lemma, and a certificate packing the claim. Experimentalists or RS auditors comparing Einstein’s law to the cost functional would cite it. Argument is definitional plus direct evaluation of J at unity.

claimFor a photoelectric material with work function $W>0$ and incident frequency $\nu$, the threshold condition is $J(W/h\nu)=0$, equivalently $h\nu=W$. Below threshold ($h\nu<W$) there is no emission. A certificate packages the material data and the identity $J(1)=0$.

background

Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain. $J(x)=0$ if and only if $x=1$ for $x>0$. The classical photoelectric effect states that electrons leave a surface only when photon energy $h\nu$ meets or exceeds the material work function $W$; Einstein’s relation is $K_{\max}=h\nu-W$.

This module imports the Cost library and rephrases the threshold as a pure cost statement: emission onsets precisely when the dimensionless ratio $W/h\nu$ sits at the unique zero of $J$. Materials are recorded as a finite enumerated type together with their work functions; the threshold and below-threshold predicates are then ordinary real inequalities rewritten via $J$.

proof idea

Definition module with thin lemmas. Materials and the certificate are data. The threshold identity reduces to $J(1)=0$, which is immediate from the closed form of $J$. The below-threshold claim is the contrapositive: if $h\nu<W$ then $W/h\nu>1$, hence $J(W/h\nu)>0$, so the cost barrier is strictly positive and emission is forbidden. No deep tactic proof; everything is algebraic evaluation of $J$ plus the ordering of the positive reals.

why it matters in Recognition Science

Places the photoelectric effect inside the single-cost ontology of Recognition Science rather than as an independent quantum postulate. Ties a textbook condensed-matter fact directly to T5 J-uniqueness and the Recognition Composition Law. Downstream physics developments that need a certified work-function threshold (photoemission spectra, RS-native units with $\hbar=\varphi^{-5}$) can import the certificate instead of re-deriving $J(1)=0$. No external parent theorems are wired yet; the module stands as a leaf that future atomic or solid-state layers can cite.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)