pith. sign in
module module moderate

IndisputableMonolith.Ethics.CostModel

show as:
view Lean formalization →

The Ethics.CostModel module defines a minimal cost model over actions of type A with nonnegative real costs. Researchers modeling ethical preferences in Recognition Science would cite it for its preference and improvement relations. The module consists of definitions and basic properties built on the imported Gap45 beat alignment rule, with no proofs.

claimLet $A$ be a type of actions. A cost model assigns to each action a cost in $mathbb{R}_{geq 0}$. Preference and improvement relations over such models satisfy reflexivity, transitivity, and compositionality.

background

The module sits in the Ethics domain and imports IndisputableMonolith.Gap45.Beat. The upstream module encodes the 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. The cost model supplies nonnegative real costs as the basis for ethical comparisons in this setting.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the cost model used in ethical applications of Recognition Science. It builds on the eight-tick octave from the Gap45 import and supports definitions for composable preferences. No downstream uses are listed, indicating it serves as a foundational interface.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)