theorem proved term proof

`zero_free_params`

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

formal statement (Lean)

  92theorem zero_free_params : per_galaxy_free_parameters = 0 := rfl

proof body

Term-mode proof.

  93
  94/-! ## SPARC Benchmark Values
  95
  96The theory document (line ~3304) gives benchmark chi2 values.
  97These are encoded as hypotheses (to be discharged by the Python script). -/
  98
  99/-- RS-predicted median chi2/dof across SPARC. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

global_only_policy in IndisputableMonolith.Gravity.SPARCFalsifier decl_use
sparc_falsifier_cert in IndisputableMonolith.Gravity.SPARCFalsifier decl_use

depends on (3)

Lean names referenced from this declaration's body.

as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
per_galaxy_free_parameters in IndisputableMonolith.Gravity.SPARCFalsifier decl_use
chi2 in IndisputableMonolith.PDG.Fits decl_use