operationsResearchCert
plain-language theorem explainer
This definition builds the OperationsResearchCert structure by wiring the five-method count to orMethodCount and the unit optimality condition to optimal_solution. Applied mathematicians treating optimization as J-cost minimization over decision spaces would cite it when embedding canonical OR techniques inside Recognition Science. The construction is a direct structure instantiation that pulls the cardinality theorem and the Jcost-unit-zero result.
Claim. The operations research certificate asserts exactly five canonical methods together with zero J-cost at unit scale: $Fintype.card(ORMethod)=5$ and $Jcost(1)=0$.
background
The module frames operations research as J-cost minimization inside Recognition Science, with the five canonical methods (linear programming, dynamic programming, game theory, queuing theory, simulation) identified with configDim D=5. Optimal solutions are defined by J=0. The upstream theorem optimal_solution states that the J-cost at unit scale vanishes, while orMethodCount establishes the cardinality of ORMethod by direct computation.
proof idea
One-line structure definition that assigns five_methods to orMethodCount and optimal to optimal_solution.
why it matters
It supplies the concrete witness that operations research reduces to J-cost minimization with method count matching D=5. The declaration closes the module by instantiating OperationsResearchCert from the two upstream results on cardinality and unit optimality. No downstream uses are recorded, but the construction supports the mapping of applied mathematics onto the Recognition Science constants and the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.