SurfacePhenomenon
plain-language theorem explainer
Recognition Science enumerates five canonical surface phenomena as an inductive type whose constructors are adsorption, desorption, surface diffusion, reconstruction, and segregation. Materials physicists modeling interfaces cite this enumeration when counting distinct processes at the canonical band in the phi-ladder framework. The declaration is a direct inductive definition that derives the Fintype instance for immediate cardinality verification in the same module.
Claim. The set of surface phenomena consists of the five elements adsorption, desorption, surface diffusion, reconstruction, and segregation, equipped with decidable equality and a finite cardinality.
background
Surface science studies interfaces between phases. In Recognition Science, surface energy equals the J-cost of the ratio of surface atoms to bulk atoms at the canonical band. The module sets five canonical surface phenomena equal to configuration dimension D = 5, with adsorption coverage given by the phi-ladder formula θ(k) = 1 - φ^{-k} at rung k.
proof idea
The declaration is a direct inductive definition that introduces the five constructors and derives the DecidableEq, Repr, BEq, and Fintype instances in a single line.
why it matters
This definition supplies the enumeration required by the downstream theorems surfacePhenomenonCount and SurfaceScienceCert, which establish that the cardinality is exactly five. It realizes the module claim that five phenomena equal configDim D = 5 and connects to the Recognition Composition Law applied at interfaces. It touches the open extension of the T0-T8 forcing chain from bulk D = 3 to surface configuration dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.