theorem proved term proof

`const_false_full_fraction`

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

formal statement (Lean)

  70theorem const_false_full_fraction (n : ℕ) :
  71    FalsePointFraction (fun _ : Fin n → Bool => false) = 1 := by

proof body

Term-mode proof.

  72  unfold FalsePointFraction
  73  simp
  74
  75/-! ## Razborov-Rudich Framework -/
  76
  77/-- A complexity property maps each arity n and truth table to a proposition. -/

depends on (5)

Lean names referenced from this declaration's body.

FalsePointFraction in IndisputableMonolith.Complexity.NonNaturalness decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use