substitutivity_from_ledger
Equal J-costs for two positive reals imply equal summed J-costs on their scaled product and quotient versions under any zero-parameter comparison ledger. Recognition theorists cite the result to close the substitutivity requirement inside the foundation without a separate axiom. The proof is a direct one-line application of the cost_sufficient field packaged in the ledger structure.
claimLet $L$ be a zero-parameter comparison ledger whose cost function is denoted $J$. If $x_1,x_2>0$ satisfy $J(x_1)=J(x_2)$ and $y>0$, then $J(x_1 y)+J(x_1/y)=J(x_2 y)+J(x_2/y)$.
background
A ZeroParameterComparisonLedger is a structure containing a nonempty countable carrier, an admissible cost function, and a conserved charge; its cost field supplies the J-cost used for recognition events. The module treats Gap 3 of the axiom-closure plan, where ledger consistency forces substitutivity as the cost_sufficient field and absorbs calibration into the Regularity Axiom. Upstream, cost is the derived cost of a multiplicative recognizer comparator or the J-cost of a recognition event, both of which inherit the same functional properties.
proof idea
The proof is a one-line wrapper that applies the cost_sufficient field of the ZeroParameterComparisonLedger to the supplied hypotheses on equal J-values and positive scaling factor.
why it matters in Recognition Science
The theorem eliminates the need for an independent substitutivity axiom in the foundation layer and thereby supports the Recognition Composition Law. It completes one step of Phase 4 in the ledger-consistency gap, feeding the forcing chain toward the eight-tick octave and three spatial dimensions. No downstream uses are recorded yet, but the result is required for any later derivation that compares costs across scaled arguments.
scope and limits
- Does not derive the explicit algebraic form of the J-cost function.
- Does not treat calibration normalization or charge conservation.
- Does not extend the equality to non-positive arguments.
- Does not address multi-agent or higher-dimensional extensions.
formal statement (Lean)
23theorem substitutivity_from_ledger
24 (L : ZeroParameterComparisonLedger)
25 (x₁ x₂ y : ℝ) (hx₁ : 0 < x₁) (hx₂ : 0 < x₂)
26 (hJ_eq : L.cost.J x₁ = L.cost.J x₂) (hy : 0 < y) :
27 L.cost.J (x₁ * y) + L.cost.J (x₁ / y) =
28 L.cost.J (x₂ * y) + L.cost.J (x₂ / y) :=
proof body
Term-mode proof.
29 L.cost_sufficient x₁ x₂ y hx₁ hx₂ hJ_eq hy
30
31/-- `λ = 1` is the unique positive real satisfying `λ = λ⁻¹`. -/