`ZeroParametersClaim`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.Constants
domain: RRF
line: 180 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RRF.Foundation.Constants on GitHub at line 180.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 177This is the formal statement of the claim. The proof would require
 178completing the full derivation chain.
 179-/
 180structure ZeroParametersClaim where
 181  /-- φ is the only input. -/
 182  input_is_phi : True
 183  /-- All constants are functions of φ. -/
 184  constants_from_phi : DerivedConstants
 185  /-- No additional parameters were introduced. -/
 186  no_free_params : True
 187
 188end RRF.Foundation
 189end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.