theorem
proved
wrapper
chain_le_creativity
show as:
view Lean formalization →
formal statement (Lean)
96theorem chain_le_creativity :
97 tierVoiceRichness .chainReasoning ≤ tierVoiceRichness .creativity := by
proof body
One-line wrapper that applies unfold.
98 unfold tierVoiceRichness; norm_num
99