Encyclopedia Ethics Ethics Moral State

ARTICLE 5 claims 3 theorems 2 models

Ethics Moral State

A moral state is a snapshot of an agent's ethical position, defined by a measurable imbalance in how they treat others.

Verify this page

Moral State in Recognition Science

In Recognition Science, a moral state is a formal snapshot of an agent's ethical position at a moment in time. It is not a subjective feeling or a cultural preference. Instead, it is a projection of the universal ledger, a discrete record of recognition events, onto one individual's domain. The state tracks two numbers: the agent's reciprocity skew σ, which measures imbalance in how they recognize others versus how others recognize them, and their available energy, which comes from the recognition cost they can still pay.

The key design choice is that ethics is grounded in physics, not arbitrary preference. The moral state wraps the foundational LedgerState structure rather than creating a parallel ethical system. The skew σ is stored in log-space, meaning it measures multiplicative imbalance additively. This matches a conservation law: for any admissible collection of states, the total skew across all agents must be zero. What one agent takes in imbalance, another must give back. The recognition cost, the forced price of each recognition event, determines how much energy an agent has available for transformations.

The framework proves several concrete facts. Energy is always positive for any moral state, and the total energy of any nonempty collection of states is also positive. A state with zero skew is called neutral, and a neutral state is balanced with itself. Two states are balanced when their skews are opposites, meaning they cancel out globally. The framework also defines a virtue as a transformation on lists of moral states that preserves global admissibility, meaning it conserves total reciprocity, and respects the eight-tick cadence, the fundamental time period from the core theorems. The identity transformation is a virtue, and virtues can be composed.

In plain language, this establishes that ethical analysis in Recognition Science is about measurable balance, not moral intuition. An agent's moral position is a number, their reciprocity skew, which must sum to zero across any admissible group. Virtues are operations that preserve this balance. The framework models ethics as a conservation law: imbalance is possible locally, but it must be paid back globally. This gives a precise, formal meaning to the idea that ethical actions have consequences that ripple through a system.

MODEL MoralState · IndisputableMonolith/Ethics/MoralState.lean
MoralState · IndisputableMonolith/Ethics/MoralState.lean:44 
/-- A moral state represents an agent's projection of the universal ledger.

    This structure connects individual ethical analysis to the underlying
    recognition ledger, ensuring morality is grounded in physics rather than
    arbitrary preferences.
-/
structure MoralState where
  /-- Underlying ledger state (contains Z-patterns, channels, global phase, time) -/
  ledger : LedgerState

  /-- Bonds controlled by this agent (subset of ledger edges).
      These bonds define the agent's domain for action and responsibility. -/
  agent_bonds : Finset BondId

  /-- Agent's local reciprocity skew σ (log-space, must sum to zero globally).

      σ measures the log-multiplier imbalance in exchanges:
      - σ > 0: agent is extracting (moral debt)
      - σ < 0: agent is contributing (moral credit)
      - σ = 0: agent is balanced (reciprocity conserved)

      Global constraint: Σ_i σ_i = 0 (enforced by `valid` field)
  -/
  skew : ℝ

  /-- Recognition cost available for transformations (from RecognitionCost).

      This tracks the J-cost capacity for ethical actions. Virtues that
      transform states must respect positive energy constraints.
  -/
  energy : ℝ

  /-- Proof: global reciprocity net skew σ = 0 (admissibility condition).

      This enforces the conservation law from Morality-As-Conservation-Law.tex:
      admissible worldlines live on the manifold where total net skew is zero.
  -/
  valid : net_skew ledger = 0

  /-- Proof: energy is positive (physical viability).

      Ensures the state is physically realizable. Negative energy would
      violate the Positive Cost principle.
  -/
  energy_pos : 0 < energy
THEOREM energy_always_positive · IndisputableMonolith/Ethics/MoralState.lean
energy_always_positive · IndisputableMonolith/Ethics/MoralState.lean:205 
/-- Energy is always positive for valid moral states -/
theorem energy_always_positive (s : MoralState) : 0 < s.energy :=
  s.energy_pos
THEOREM total_energy_positive_of_nonempty · IndisputableMonolith/Ethics/MoralState.lean
total_energy_positive_of_nonempty · IndisputableMonolith/Ethics/MoralState.lean:232 
/-- Total energy is positive if any state has positive energy -/
theorem total_energy_positive_of_nonempty (states : List MoralState)
  (h : states ≠ []) :
 0 < MoralState.total_energy states := by
  -- Helper: total energy is always nonnegative.
  have total_nonneg : ∀ xs, 0 ≤ MoralState.total_energy xs := by
    intro xs
    induction xs with
    | nil =>
        simp [MoralState.total_energy]
    | cons s ss ih =>
        have hs : 0 ≤ s.energy := le_of_lt s.energy_pos
        have hrec : MoralState.total_energy (s :: ss) =
            s.energy + MoralState.total_energy ss := by
          change List.foldl (fun a t => a + t.energy) 0 (s :: ss)
              = s.energy + List.foldl (fun a t => a + t.energy) 0 ss
          simp [List.foldl]
          -- reduce to foldl starting at s.energy, then apply helper lemma
          simpa [add_comm] using (total_energy_foldl_add_const ss s.energy)
        have : 0 ≤ s.energy + MoralState.total_energy ss := add_nonneg hs ih
        simpa [hrec]
  -- Main argument by cases.
  cases states with
  | nil => cases h rfl
  | cons s ss =>
      have hs_pos : 0 < s.energy := s.energy_pos
      have hss_nonneg : 0 ≤ MoralState.total_energy ss := total_nonneg ss
      have : 0 < s.energy + MoralState.total_energy ss :=
        add_pos_of_pos_of_nonneg hs_pos hss_nonneg
      have hrec : MoralState.total_energy (s :: ss) =
          s.energy + MoralState.total_energy ss := by
        change List.foldl (fun a t => a + t.energy) 0 (s :: ss)
            = s.energy + List.foldl (fun a t => a + t.energy) 0 ss
        simp [List.foldl]
        simpa [add_comm] using (total_energy_foldl_add_const ss s.energy)
      simpa [hrec]
MODEL Virtue · IndisputableMonolith/Ethics/MoralState.lean
Virtue · IndisputableMonolith/Ethics/MoralState.lean:286 
/-- Virtue structure representing a transformation on moral states. -/
structure Virtue where
  /-- The transformation (may be single-agent or multi-agent) -/
  transform : List MoralState → List MoralState

  /-- Preserves or restores global reciprocity conservation (σ=0). -/
  conserves_reciprocity : ∀ states : List MoralState,
    MoralState.globally_admissible states →
    MoralState.globally_admissible (transform states)

  -- Former fields `minimizes_local_J : ∀ states, True` and
  -- `gauge_invariant : ∀ states, True` deleted (Move A). Both names promised
  -- ethical constraints and excluded nothing. Local J-minimization is proved
  -- per virtue where available (e.g. `love_minimizes_squared_skew`);
  -- unit-gauge independence is structural because `MoralState` carries no
  -- (τ₀, ℓ₀) parameters. Do not restore as concl-True fields.

  /-- Respects eight-tick cadence (fundamental period from T6).
      Requires TimeCoherent precondition on input states. -/
  respects_cadence : ∀ states : List MoralState,
    TimeCoherent states →
    let states' := transform states
    ∀ s ∈ states, ∀ s' ∈ states',
      s'.ledger.time - s.ledger.time ≤ 8
THEOREM identityVirtue · IndisputableMonolith/Ethics/MoralState.lean
identityVirtue · IndisputableMonolith/Ethics/MoralState.lean:313 
/-- Identity virtue: does nothing, trivially preserves all properties -/
def identityVirtue : Virtue where
  transform := id
  conserves_reciprocity := fun _ h => h
  respects_cadence := fun states h_coh s hs s' hs' => by
    -- For identity, states' = states, so s' ∈ states
    -- Use time-coherence: any two states in the list have times within 8 ticks
    have := h_coh s hs s' hs'
    exact this.1

What this page does not claim

This does not claim that moral state is a complete theory of ethics or that it captures all moral considerations. This does not claim that the conservation law has been empirically verified in human societies. This does not claim that the framework defines what actions are right or wrong, only what states are admissible.

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/Ethics/MoralState.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND