OperationsResearchCert
plain-language theorem explainer
OperationsResearchCert packages the assertion that exactly five operations research methods exist in the Recognition Science setting together with the fact that minimum J-cost is zero. Applied mathematicians and economists working on optimization problems would cite this certificate when connecting standard OR techniques to J-cost minimization. The structure is defined directly with two fields, one for the cardinality of the ORMethod type and one for the optimal cost condition.
Claim. A structure certifying that the number of canonical operations research methods is five and that the J-cost of the unit decision equals zero.
background
The module presents operations research as applied mathematics derived from Recognition Science. Optimization is defined as minimization of J-cost over the decision space, with the optimal solution occurring where J-cost reaches zero. The five canonical methods (linear programming, dynamic programming, game theory, queuing theory, simulation) are identified with configuration dimension D equal to five.
proof idea
The declaration is a structure definition with two fields and no proof body. The first field encodes the cardinality of the ORMethod inductive type, which has exactly five constructors. The second field states the equality Jcost 1 = 0, supplied downstream by optimal_solution.
why it matters
This certificate links the five operations research methods to the Recognition Science J-cost framework and confirms that their count matches configuration dimension five while the minimum cost is zero. It is instantiated by the operationsResearchCert definition, which populates the fields from orMethodCount and optimal_solution. The result supports the reduction of optimization problems to J-cost minimization in the broader forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.