Explain the Lean theorem `recidivismCost_at_equilibrium` in module `IndisputableMonolith.CriminalJustice.RecidivismFromJCost`. Write for an educated reader who knows science and programming but may not know Lean. Cover: (1) what the declaration says in plain English, (2) why it matters in Recognition Science, (3) how to read the formal statement, (4) visible dependencies or certificates in the supplied source, and (5) what this declaration does not prove. Cite only declarations present in the supplied Recognition source.

1. Plain English

The declaration recidivismCost_at_equilibrium states that if a rehabilitation program has no effect—meaning the post-intervention reoffense rate equals the pre-intervention baseline rate (and the rate is non-zero)—the calculated "recidivism cost" evaluates to exactly zero.

2. Why it matters in Recognition Science

In Recognition Science, structural departures from an equilibrium state incur a mathematical "recognition cost" governed by the J(x) functional equation. This THEOREM establishes the absolute floor: a system at equilibrium (a ratio of 1) generates no new structural information and incurs zero cost.

As the module's docstring outlines, when an intervention does work, the ratio of reoffense to baseline drops below 1. This generates a positive J-cost. The RS framework generates a HYPOTHESIS that the minimum detectable societal shift in recidivism corresponds to a single quantum step on the recognition ladder, costing J(φ) ≈ 0.118.

3. How to read the formal statement

theorem recidivismCost_at_equilibrium (r : ℝ) (h : r ≠ 0) :
    recidivismCost r r = 0

• r : ℝ and h : r ≠ 0: Let r be any non-zero real number (representing the baseline and reoffense rate).
• recidivismCost r r = 0: When r is supplied as both the reoffense and baseline arguments to the recidivismCost MODEL, the result is exactly 0.

4. Visible dependencies and certificates

The proof operates by unfolding the definition of recidivismCost, rewriting the fraction r / r to 1 (which requires the proof h that r ≠ 0), and invoking the external theorem Jcost_unit0 (which states J(1) = 0).

This theorem is directly utilized to satisfy the cost_at_equilibrium field of RecidivismCert. This certificate mathematically verifies that the recidivism cost model obeys the necessary symmetries and zero-points required to act as a valid RS partition variable.

5. What this declaration does not prove

This declaration is a structural THEOREM about a defined function; it does not prove:

• The actual value of the discrete recognition threshold (this is handled by recidivismCost_phi_step, which proves J(φ) = φ - 3/2).
• That human recidivism statistics empirically lock into these specific mathematical ratios. The module explicitly defines this as a falsifiable prediction requiring large-N randomized controlled trials.
• The underlying properties of Jcost itself, which are imported from the IndisputableMonolith.Cost namespace.