SurfaceScienceCert
plain-language theorem explainer
SurfaceScienceCert is a structure that records the fact that the inductive enumeration of surface phenomena has cardinality exactly five. Materials physicists applying Recognition Science to interfaces cite it when anchoring adsorption, desorption, surface diffusion, reconstruction and segregation to the configuration dimension of the theory. The structure is realized directly by the Fintype instance carried by the inductive type.
Claim. Let $P$ be the finite set whose elements are adsorption, desorption, surface diffusion, reconstruction and segregation. The structure SurfaceScienceCert consists of the single datum witnessing $|P|=5$.
background
Recognition Science treats surface energy as the J-cost of the ratio of surface atoms to bulk atoms evaluated inside the canonical band. The module isolates five canonical interface processes and collects them in the inductive type SurfacePhenomenon, which derives DecidableEq, Repr, BEq and Fintype. The local theoretical setting equates this count with configDim D=5, the dimension required by the Recognition Composition Law for surface configurations. The upstream inductive declaration supplies the Fintype instance used by the cardinality field.
proof idea
The declaration is a structure definition whose single field directly records the cardinality of the inductive type SurfacePhenomenon. No lemmas or tactics are invoked; the Fintype derivation is inherited from the inductive declaration of the five constructors.
why it matters
SurfaceScienceCert supplies the certificate consumed by the downstream definition surfaceScienceCert. It closes the link between the Recognition Science forcing chain (T0-T8) and concrete surface phenomena, where the count five matches the configuration dimension needed for the surface-energy formula and the phi-ladder coverage relation θ(k)=1-φ^{-k}. The structure therefore anchors the five-tick surface sector to the same self-similar fixed-point machinery that forces D=3 in the bulk.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.