of
plain-language theorem explainer
Recognition Science classifies the computational complexity of physics through the structure of J-cost minimization, which lists convexity of J with minimum at unity, O(1) local 8-tick updates, linear-time ground-state verification, and exponential cost for phi-rung states. Complexity theorists mapping physical models to classes such as P or EXPTIME would cite this when locating RS-derived dynamics in the zoo. The definition enumerates the four properties directly from J-cost and tick primitives.
Claim. The structure of J-cost minimization comprises four properties: (1) the function $J(x) = (x + x^{-1})/2 - 1$ is strictly convex with unique global minimum at $x=1$; (2) each tick updates at most eight local neighbors, making dynamics O(1) per step; (3) verifying a balanced ledger requires O(N) bond checks; (4) phi-rung mass computations scale exponentially with rung index.
background
The module addresses the placement of Recognition Science physics in the complexity zoo by analyzing J-cost minimization. J-cost is the non-negative function minimized at recognition equilibrium, with its convexity and derivative properties established in sibling declarations such as jcost_nonneg and jcost_deriv. The eight-tick period is the fundamental evolution interval defined by Constants.tick, while local updates draw on the neighborhood extraction in CellularAutomata.step. Upstream results include the rung indexing in Compat.Constants and the tiered densities in NucleosynthesisTiers.of, which supply the phi-hierarchy growth.
proof idea
This is a definition that directly enumerates the four complexity properties without a proof body. It assembles the claims from the J-cost convexity facts in the Cost module, the locality lemma in CellularAutomata.step, and the tick definition in Constants.tick. No tactics are applied; the structure serves as a named container for the listed assertions.
why it matters
The structure supplies the complexity profile that downstream declarations in Action.EulerLagrange and Acoustics.SpeechIntelligibilityFromJCost rely upon when invoking J-cost positivity and geodesic properties. It realizes the IC-005 claim stated in the module documentation, connecting to the eight-tick octave and phi-ladder mass formula. It leaves open the formalization of the NP-hard analog for global optimization over ledger states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.