validationSubstrateCount
plain-language theorem explainer
The theorem states that the finite type enumerating the three experimental substrates for J-cost validation has cardinality three. Researchers assembling the Recognition Science three-substrate certificate would cite it to anchor the enumeration in the Lean model. The proof is a single decision tactic that evaluates the cardinality directly from the derived Fintype instance on the inductive definition.
Claim. Let $V$ be the finite type whose elements are the language-model, photonic-qubit, and magnetized-plasma substrates. Then $|V| = 3$.
background
The module ThreeSubstrateValidationCert models the empirical validation of J-cost across three substrates, as summarized in its documentation: language models (96.4% beat of CE), photonic qubits (code rate 7/8), and magnetized plasma (convergence to x=1.036). All three are asserted to share the fixed point at x=1 where J(1)=0, the descent direction from the J-cost gradient, and the multi-channel extension. ValidationSubstrate is the inductive type with constructors languageModel, photonicQubit, magnetizedPlasma that derives Fintype, DecidableEq, Repr, and BEq. Upstream cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost used in the broader certificate but are not invoked by this count.
proof idea
The proof is a term-mode application of the decide tactic. It succeeds because the inductive definition of ValidationSubstrate derives an instance of Fintype whose cardinality is statically three.
why it matters
The result supplies the three_substrates field of the ThreeSubstrateCert structure, which aggregates the shared fixed point, descent, symmetry, and language-model alignment across the substrates. It directly implements the module claim that J-cost uniqueness underlies all three experimental channels. The declaration sits at the interface between the T5 J-uniqueness landmark and the hypothesis-grade empirical certificate in RS Exp B.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.