pith. machine review for the scientific record. sign in
def definition def or abbrev high

action_raw

show as:
view Lean formalization →

This definition converts an action count expressed in act units to the raw real-number scale used throughout the RS-native system. Researchers expressing physical quantities directly in ledger primitives would apply it when scaling action by the fundamental quantum. It is implemented as a direct multiplication by the pre-established action quantum.

claimThe raw action in RS-native units is obtained by scaling the input count: if A denotes the action measured in act units, then the result equals A multiplied by the action quantum ħ, where ħ equals the coherence energy times the tick interval.

background

The RS-native measurement system takes the tick (one discrete ledger interval) and voxel (spatial step at unit speed) as base units, with c fixed at 1. Derived quanta are the coherence energy E_coh = φ^{-5} and the action quantum ħ = E_coh · τ₀, which numerically equals E_coh in these units. All quantities are expressed on the φ-ladder without reference to SI anchors.

proof idea

One-line definition that multiplies the input Action count by the value of hbarQuantum.

why it matters in Recognition Science

The definition supplies the scaling map that places action on the same numerical footing as the coherence and actualization operators used elsewhere in the framework. It directly supports the module goal of writing all physics in tick/voxel units where the action quantum is ħ = E_coh · τ₀. No downstream theorems are recorded yet.

scope and limits

formal statement (Lean)

 107@[simp] noncomputable def action_raw (A : Action) : ℝ := A * hbarQuantum

proof body

Definition body.

 108

depends on (5)

Lean names referenced from this declaration's body.