orMethodCount
plain-language theorem explainer
Establishes that the finite type of operations research methods has cardinality 5. Researchers in Recognition Science applied mathematics cite this to confirm configDim D equals 5 for the decision space. The proof is a direct decidable computation on the inductive type with five constructors.
Claim. The finite set enumerating linear programming, dynamic programming, game theory, queuing theory, and simulation has cardinality 5.
background
The module treats operations research as an application of Recognition Science where optimization minimizes J-cost over a decision space of dimension configDim D = 5. The optimal solution occurs at J = 0. The upstream inductive definition enumerates the methods as linear programming, dynamic programming, game theory, queuing theory, and simulation, automatically deriving the Fintype instance required for cardinality computation.
proof idea
A one-line wrapper that invokes the decide tactic to evaluate the cardinality of the finite inductive type.
why it matters
This theorem populates the five_methods field in the downstream OperationsResearchCert definition, which also records the optimal J = 0 solution. It thereby embeds the standard count of five methods into the Recognition Science framework as a consequence of the configuration dimension. The result supports the claim that applied mathematics emerges from the same functional equation that yields the forcing chain and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.