pathIntegralCount
plain-language theorem explainer
The theorem establishes that the inductive enumeration of path integral formulations contains exactly five members. Researchers deriving the Feynman path integral from the J-cost functional in Recognition Science would cite this count to fix the configuration dimension. The proof is a one-line decision procedure that exhausts the finite type constructors.
Claim. The set of canonical path integral formulations has cardinality five.
background
The module reinterprets the Feynman path integral as a sum over J-cost weighted recognition paths, with the classical trajectory at the J-cost minimum of zero. It introduces an inductive enumeration of five formulations: position, momentum, coherent state, field theory, and string representations, matching the configuration dimension of five. This builds directly on the point definition for single-rational intervals from the numerics module, which supplies the underlying interval arithmetic for cost calculations.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card computation on the enumerated type, which directly verifies the cardinality from its five constructors.
why it matters
This supplies the five_formulations field in the path integral certificate definition downstream. It anchors the RS-native path integral to five canonical representations, consistent with the module's reinterpretation of Z as a sum over J-cost paths and the framework emphasis on discrete enumeration before continuum limits. No open questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.