ValidationSubstrate
plain-language theorem explainer
The inductive type enumerates the three substrates on which J-cost is validated in Recognition Science Exp B. Researchers working with the three-substrate certificate cite this enumeration to index the shared empirical predictions. It is introduced directly as an inductive definition with three constructors and the standard DecidableEq, Repr, BEq, Fintype derivations.
Claim. Let $S$ be the finite set of validation substrates. Then $S$ consists of the three elements language models, photonic qubits, and magnetized plasma.
background
The module ThreeSubstrateValidationCert records the empirical validation of J-cost across three substrates. J-cost is the function satisfying the Recognition Composition Law and the fixed-point condition J(1) = 0. The module doc states that all three substrates share the same predictions: fixed point at x = 1, descent from the J-cost gradient, and validity of the multi-channel extension. No upstream lemmas are required; the declaration depends on nothing inside the module.
proof idea
This is an inductive definition with three constructors and the listed typeclass derivations. No tactics or lemmas are applied; the declaration simply enumerates the substrates.
why it matters
The type supplies the domain for the structure ThreeSubstrateCert, which asserts Fintype.card = 3 together with the shared properties Jcost 1 = 0, descent for r ≠ 1, symmetry under inversion, and languageModelAlignmentFraction = 7/8. It therefore anchors the hypothesis-grade certificate that J-cost uniqueness (T5) holds uniformly across language-model, photonic, and plasma substrates. The declaration closes the enumeration step required before the cardinality theorem validationSubstrateCount can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.