theorem proved term proof

`improves_comp_left`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  60theorem improves_comp_left (M : CostModel A) (C : Composable M)
  61  {a b x : A} (h : Improves M a b) : Improves M (C.comp a x) (C.comp b x) := by

proof body

Term-mode proof.

  62  exact C.strict_mono_left a b x h
  63
  64/-- CQ alignment at threshold θ ∈ [0,1]: score ≥ θ. -/
  65/- Placeholder removed: use concrete CQ and score from Measurement. -/

depends on (21)

Lean names referenced from this declaration's body.

comp in IndisputableMonolith.Algebra.CostAlgebra decl_use
Measurement in IndisputableMonolith.Data.Import decl_use
Composable in IndisputableMonolith.Ethics.CostModel decl_use
CostModel in IndisputableMonolith.Ethics.CostModel decl_use
CQ in IndisputableMonolith.Ethics.CostModel decl_use
Improves in IndisputableMonolith.Ethics.CostModel decl_use
score in IndisputableMonolith.Ethics.CostModel decl_use
comp in IndisputableMonolith.Foundation.ArithmeticOf decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
CQ in IndisputableMonolith.Measurement decl_use
score in IndisputableMonolith.Measurement decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use
comp in IndisputableMonolith.RRF.Core.Octave decl_use
comp in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use