path_action_single
plain-language theorem explainer
The lemma states that a singleton path has action equal to the J-cost of its configuration value. Modal actualization arguments cite this base case when defining path weights that produce the Born rule via exponential damping of total cost. The proof is a direct reflexivity reduction on the PathAction definition for the one-element list.
Claim. For a configuration $c$, the path action of the singleton list $[c]$ equals $J(c.value)$.
background
PathAction is defined as the total J-cost accumulated along a path of configurations: the empty path gives zero, a singleton reduces to J of the value, and longer paths add J terms plus transition costs between consecutive positions. The Modal.Actualization module uses this to ground actualization of configurations in the Recognition framework. Upstream calibration of J appears in PhiForcingDerived.of and DAlembert.LedgerFactorization.of, which fix the cost function from the Recognition Composition Law.
proof idea
The proof is a one-line term proof that applies reflexivity directly to the singleton clause in the definition of PathAction.
why it matters
This base case anchors the definition of PathWeight, whose exponential form W[γ] = exp(-C[γ]) supplies the Born rule in the modal setting. It sits inside the forcing chain after T5 J-uniqueness and supports the eight-tick octave structure by treating single configurations as minimal actualized units. No open scaffolding is closed here; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.