Foundation Ethics

The ethical ledger

Foundation ethics in Recognition Science is the attempt to treat justice as a bookkeeping problem. The framework's core idea is a ledger, a discrete record of events, where every action carries a forced cost. In ethics, that cost is applied to the ratio of harm repaired to harm done. The central definition is simple: the cost function J, applied to the quotient m/e, where m is the measure of repair and e is the measure of the original harm. When repair exactly matches harm, the ratio is 1, and the cost is zero. When repair falls short, the cost is positive.

The module proves three general facts about this cost. First, when the ratio is 1, the cost is exactly zero: full repair has zero residual cost. Second, for any positive amounts of harm and repair, the cost is never negative; you cannot get credit for making things worse. Third, the threshold value phi minus 3/2 is positive, where phi is the golden ratio, about 1.618. This threshold is proposed as the boundary between acceptable partial restoration and unacceptable failure to repair. The three facts together form a certificate, a machine-checked proof that the cost function behaves as a restorative justice metric should.

What the module does not do is as important as what it proves. The cost function is defined generically, without specifying what m and e mean in any particular ethical context. The same formal template is shared verbatim with 2383 sibling modules. The proofs establish properties of the cost function itself, not of any concrete justice system. To make this a theorem about restorative justice, one would need to define m and e in the terms of that subject: what counts as harm, what counts as repair, and how they are measured.

In Recognition Science, the framework models restoration as complete when the cost reaches zero, meaning repair fully balances harm. Partial restoration leaves a positive cost, but one that stays below the golden-ratio threshold is considered acceptable. This gives a formal language for talking about degrees of repair, but the framework itself is explicit that the translation from abstract cost to real-world ethics remains a research note, not a result. The plain-language takeaway is that the mathematics provides a consistent, nonnegative measure of repair shortfall, and a named threshold for acceptability, while the hard question of what to measure remains open.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The module proves nothing about any specific ethical subject or real-world justice system. The framework does not derive the golden-ratio threshold from ethical first principles; it is a proposed definition. This is not a claim that the cost function uniquely characterizes restorative justice.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/Ethics.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: