`cert`

definition

show as: view math explainer →

module: IndisputableMonolith.Common.CanonicalJBand
domain: Common
line: 84 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Common.CanonicalJBand on GitHub at line 84.

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

  81  phi_band : (0.11 : ℝ) < J phi ∧ J phi < 0.13
  82  recovery_pos : J (1 / phi ^ 2) > 0
  83
  84def cert : CanonicalCert where
  85  matched_zero := J_one
  86  reciprocal := J_reciprocal
  87  phi_pos := J_phi_pos
  88  phi_band := J_phi_band
  89  recovery_pos := J_inv_phi_sq_pos
  90
  91end
  92
  93end CanonicalJBand
  94end Common
  95end IndisputableMonolith

papers checked against this theorem

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