Action
plain-language theorem explainer
Action supplies the real-number carrier type for action quantities in the RS-native unit system. Researchers deriving energy conservation or Euler-Lagrange equations cite it when expressing the J-action functional in tick/voxel units. The declaration is a direct abbreviation with no computational content.
Claim. In the Recognition Science native unit system, action is represented by elements of $ℝ$, with the fundamental scale fixed by $ħ = φ^{-5}$ in coherence units where $c = 1$.
background
The module establishes an RS-native measurement system whose base units are the tick (one discrete ledger interval) and the voxel (distance light travels in one tick). Derived quanta are the coherence energy $E_{coh} = φ^{-5}$ and the action quantum $ħ = E_{coh} · τ_0$. All physical quantities, including action, are expressed as real numbers on the φ-ladder with $c = 1$ and all dimensionless ratios determined by φ alone.
proof idea
Direct abbreviation to the real numbers; no lemmas or tactics are applied.
why it matters
Action supplies the type used by EnergyConservationCert, eulerLagrange_status, hamiltonian_status and functionalConvexity_status to state conservation and variational results for the J-action. It anchors the framework's treatment of action as the native ħ, consistent with the phi-ladder and the eight-tick octave, and enables the downstream derivation of constants such as $G = φ^5 / π$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.