validationSubstrateCount
plain-language theorem explainer
The theorem states that the finite type of validation substrates has cardinality three. Researchers citing the three-substrate validation certificate in Recognition Science use it to anchor the enumeration of language models, photonic qubits, and magnetized plasma. The proof is a one-line decision procedure that evaluates the cardinality directly from the inductive constructors.
Claim. The finite type consisting of the three validation substrates (language model, photonic qubit, magnetized plasma) has cardinality three.
background
The Three-Substrate Validation Certificate module validates J-cost across three substrates drawn from language models, photonic qubits, and magnetized plasma. The ValidationSubstrate inductive type enumerates these three cases and derives Fintype, DecidableEq, and related instances to support cardinality and equality computations. Upstream, the cost definition from MultiplicativeRecognizerL4 gives the derived cost of a comparator on positive ratios, while the cost from ObserverForcing is the J-cost of a recognition event; the point constructor from Interval.Basic supplies singleton rational intervals for numerical checks. The module states that the certificate remains at hypothesis grade, with the Lean content confirming structural uniqueness of the J-cost fixed point at x=1.
proof idea
The proof is a one-line term proof that applies the decide tactic. The tactic computes Fintype.card directly from the inductive definition of ValidationSubstrate, which contains exactly three constructors, and reduces the equality to a decidable proposition that evaluates to true.
why it matters
This theorem populates the three_substrates field of the ThreeSubstrateCert structure, which aggregates fixed_point, descent, symmetry, and alignment data across the substrates. It supports the module's claim that all three substrates share the J-cost fixed point at x=1 and the same descent direction from the J-cost gradient. In the Recognition Science framework it closes the structural part of the hypothesis-grade certificate for the multiplicative recognizer and observer forcing costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.