PhotoelectricMaterial
plain-language theorem explainer
This inductive type enumerates the five canonical materials for the Recognition Science J-cost model of the photoelectric effect. Researchers deriving threshold frequencies from the J functional would cite it to fix the configuration dimension at five. The definition is a direct inductive enumeration equipped with Fintype derivation, enabling immediate cardinality computation.
Claim. Let $M$ be the finite set of photoelectric materials consisting of sodium, potassium, cesium, rubidium, and gold.
background
In the Recognition Science treatment, the photoelectric effect is expressed via the J-cost of normalized photon energy: electrons are ejected precisely when this cost vanishes. The module states that at threshold J(W/hν) = 0, below threshold the cost is positive, and the five listed materials fix configDim D = 5. The definition supplies the concrete finite set on which these statements are evaluated.
proof idea
The declaration is a direct inductive definition of five constructors with automatic derivation of DecidableEq, Repr, BEq, and Fintype instances.
why it matters
The type supplies the finite set required by the downstream PhotoelectricCert structure, which asserts Fintype.card PhotoelectricMaterial = 5 together with the threshold condition Jcost 1 = 0. It anchors the model to the standard experimental materials and connects to the Recognition framework where configuration dimensions are fixed by such enumerations. The sibling theorem photoelectricMaterialCount computes the cardinality by decision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.