NewtonianParticle
plain-language theorem explainer
NewtonianParticle supplies the target structure for a classical point particle with real position, velocity, and mass. Researchers deriving Newton's laws inside the Recognition Science J-cost framework cite it when showing that F = ma arises as the minimum-cost path after coarse-graining. The declaration is a bare structure definition carrying only three real fields and an attached explanatory comment.
Claim. A Newtonian particle is a triple $(x, v, m) ∈ ℝ³$ in which $x$ is position, $v$ is velocity, and $m$ is mass; the triple is the configuration that realizes minimum total J-cost on the coarse-grained ledger.
background
The module QF-011 treats classical emergence as the outcome of many-body J-cost minimization. Product states incur J-cost linear in particle number N while entangled states scale as N² or worse, so the large-N limit selects classical product states. Cost is supplied by upstream definitions: cost of a recognition event equals Jcost of its state, and the multiplicative-recognizer cost is the derived cost of its comparator on positive ratios. LedgerFactorization calibrates J on the multiplicative monoid of positive reals.
proof idea
Direct structure definition. The three fields x, v, m are introduced as real numbers with no computational content or proof obligations; an attached comment records the intended link to least-action expressed as J-cost minimization.
why it matters
The structure anchors the classical-limit target inside the QF-011 program. It supplies the concrete object for later derivations that obtain F = ma from J-cost paths once coarse-graining has occurred. The construction sits downstream of phi-forcing, observer-cost, and ledger-factorization machinery and supports the claim that Newton's laws appear precisely when many-body J-cost selects product states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.