pith. sign in
module module high

IndisputableMonolith.Ethics.CostModel

show as:
view Lean formalization →

The Ethics.CostModel module supplies a minimal cost model over an arbitrary action type A, with costs required to be nonnegative reals. Decision theorists or ethicists working inside the Recognition Science framework cite it when formalizing preference and improvement relations. The module is purely definitional, importing the Gap45.Beat alignment rule to ground its ethical constructions.

claimLet $A$ be a type of actions. A cost model is any function $c:A o\mathbb{R}_{\geq0}$.

background

The module opens the ethics domain inside Recognition Science. Its sole import is IndisputableMonolith.Gap45.Beat, whose doc-comment states: "Gap45 gating rule: experience is required exactly when the plan period is not a multiple of 8. This captures the Source.txt policy that 8-beat alignment disables Gap45 gating." Sibling declarations introduce CostModel, Prefer, Improves, Composable, CQ, score, and CQAligned, all built on the nonnegative-real cost assumption.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the base cost model that ethics constructions rely on. It feeds the eight-tick octave (T7) alignment policy through its Gap45.Beat import and positions ethical costs inside the Recognition framework's forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)