IndisputableMonolith.Robotics.PIDStabilityFromJCost
The module defines recognition descent for self-maps on positive reals and assembles supporting notions of trajectories and cost steps to certify PID stability via J-cost decrease. Control theorists linking Recognition Science to feedback design would cite the resulting stability statements. The module structures its content as a sequence of definitions and lemmas around the core descent predicate.
claimA self-map $f:(0,∞)→(0,∞)$ exhibits recognition descent when $f(1)=1$ and $J(f(r))<J(r)$ for every $r>0$ with $r≠1$, where $J$ is the J-cost.
background
The module resides in the Robotics subdomain and imports the base time quantum τ₀=1 tick from Constants together with the J-cost from the Cost module. Recognition descent is introduced exactly as the property that fixes the equilibrium at unity while enforcing strict J-cost decrease elsewhere. Auxiliary objects include trajectory sequences that track iterated application of the map and lemmas that isolate cost positivity off equilibrium.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the recognition descent predicate and the PIDStabilityCert together with the one-statement stability result. It extends the J-uniqueness property from the forcing chain into control applications while remaining inside RS-native units. No downstream users are recorded yet.
scope and limits
- Does not derive the explicit form of the J-cost function.
- Does not treat discrete-time or sampled-data implementations.
- Does not incorporate sensor noise or external forcing terms.
- Does not supply numerical convergence rates or gain bounds.
depends on (2)
declarations in this module (12)
-
structure
RecognitionDescent -
def
trajectory -
theorem
trajectory_zero -
theorem
trajectory_succ -
theorem
trajectory_at_equilibrium -
theorem
trajectory_pos -
theorem
cost_descent_step -
theorem
cost_zero_iff_equilibrium -
theorem
cost_pos_off_equilibrium -
structure
PIDStabilityCert -
def
pidStabilityCert -
theorem
pid_stability_one_statement