path_action_single
plain-language theorem explainer
A singleton path consisting of one configuration c has total action equal to the J-cost of its value. Modal actualization arguments in Recognition Science cite this base case when collapsing single-step paths to the underlying cost function. The proof is a one-line reflexivity that matches the singleton clause in the PathAction definition.
Claim. For any configuration $c$, the action of the singleton path $[c]$ equals $J(c.value)$.
background
PathAction is the total J-cost accumulated along a path of configurations: zero on the empty list, J of the single value on a singleton list, and the sum of individual J terms plus J_transition costs on longer lists. The Actualization module develops the ActualizationPrinciple and related notions of path actualization in a modal setting, importing the Possibility module. Upstream results supply the structure of J-cost (PhiForcingDerived.of) and ledger factorizations that calibrate the cost function.
proof idea
One-line term proof by reflexivity that matches the singleton case of the PathAction definition.
why it matters
This lemma supplies the base case for PathAction inside the Actualization module and thereby supports the definition of path weights W[γ] = exp(-C[γ]) that give rise to the Born rule. It sits downstream of the J-uniqueness result (T5) and feeds the broader actualization machinery that connects modal paths to the Recognition Composition Law and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.