PathIntegralFormulation
plain-language theorem explainer
Recognition Science encodes the five standard formulations of the Feynman path integral as an inductive type whose cardinality equals five. A physicist mapping the path integral onto J-cost weighted recognition paths would cite this enumeration when establishing the configuration dimension. The definition directly lists the five cases and derives Fintype, so the cardinality follows by computation.
Claim. The set of canonical path-integral formulations consists of five elements: the position-space formulation, the momentum-space formulation, the coherent-state formulation, the field-theoretic formulation, and the string-theoretic formulation.
background
In Recognition Science the Feynman path integral is reinterpreted as a sum over recognition paths weighted by the J-cost function. The classical trajectory is the path of minimum J-cost (equal to zero), while any deviation carries strictly positive J-cost. The module fixes the configuration dimension at five and enumerates the five standard formulations that realize this dimension.
proof idea
Direct inductive definition that enumerates the five cases and derives the Fintype instance; cardinality is then obtained by the decide tactic in the downstream count theorem.
why it matters
This definition supplies the domain required by PathIntegralCert, which records that exactly five formulations exist, that the classical path has J-cost zero, and that quantum paths have positive J-cost. It therefore anchors the translation of the standard path integral into the RS-native J-cost weighting and feeds the explicit cardinality result pathIntegralCount.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.