photoelectricMaterialCount
plain-language theorem explainer
The theorem fixes the number of photoelectric materials at exactly five in the Recognition Science J-cost model. Physicists deriving threshold frequencies from work functions would cite this count when enumerating the canonical alkali and noble metals. The proof is a one-line decide tactic that exhausts the finite inductive type.
Claim. The set of photoelectric materials has cardinality five: $|$sodium, potassium, cesium, rubidium, gold$| = 5$.
background
The module models the photoelectric effect via the J-cost: electrons eject when photon energy exceeds the work function W, with threshold condition J(W/hν) = 0 implying exact equality hν = W. Below threshold J > 0 blocks ejection; above threshold the excess energy yields J > 0 on the remainder. Five canonical materials (alkali Na/K/Cs/Rb plus noble Au) are declared to equal configDim D = 5.
proof idea
The proof is a term-mode one-liner that applies the decide tactic. The tactic evaluates Fintype.card on the inductive type whose five constructors are sodium, potassium, cesium, rubidium and gold, returning the literal 5.
why it matters
The result supplies the five_materials field to the downstream photoelectricCert definition that certifies the full J-cost photoelectric model. It realizes the framework assignment of five materials to configDim D = 5 and closes the enumeration step in the derivation of the photoelectric threshold, consistent with the Recognition Composition Law and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.