PhotoelectricCert
plain-language theorem explainer
PhotoelectricCert packages the five canonical materials, the exact threshold Jcost(1)=0, and Jcost positivity for r>0 with r≠1 into a single record. A physicist deriving the photoelectric effect inside Recognition Science would cite this structure to certify that the J-cost model reproduces the observed cutoff for alkali and noble metals. The definition is a direct aggregation of three facts already proved elsewhere in the module.
Claim. A record asserting that the inductive type of photoelectric materials (sodium, potassium, cesium, rubidium, gold) has cardinality five, that $J(1)=0$, and that $J(r)>0$ for every real $r>0$ with $r≠1$.
background
The module shows that the photoelectric effect follows from the J-cost function: the work function W corresponds to the point where J(W/E_photon) vanishes. PhotoelectricMaterial is the inductive type with exactly those five constructors. The upstream below_threshold theorem states that Jcost r > 0 whenever r > 0 and r ≠ 1, proved by direct appeal to Jcost_pos_of_ne_one.
proof idea
This is a structure definition with an empty proof body. It simply declares three fields whose types are supplied by the cardinality of PhotoelectricMaterial, the threshold equality, and the already-proved below_threshold theorem.
why it matters
The structure is instantiated by the downstream photoelectricCert definition, which supplies the concrete values. It embeds the J-cost threshold behavior into the Recognition Science account of the photoelectric effect, confirming that the five materials match the configuration dimension D=5 and that positivity of J away from unity enforces the experimental cutoff. The construction closes one link between the functional equation for J and classical optics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.