theorem proved term proof

`perBitCost_pos`

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

formal statement (Lean)

  44theorem perBitCost_pos : 0 < perBitCost :=

proof body

Term-mode proof.

  45  Real.log_pos one_lt_phi
  46
  47/-! ## §2. Total J-cost of n-bit key recovery -/
  48
  49/-- Total J-cost of recovering an `n`-bit key (additive over bits). -/

used by (4)

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

cryptography_one_statement in IndisputableMonolith.Cryptography.RSCryptographicBound decl_use
rSCryptographicBoundCert in IndisputableMonolith.Cryptography.RSCryptographicBound decl_use
totalRecoveryCost_pos in IndisputableMonolith.Cryptography.RSCryptographicBound decl_use
totalRecoveryCost_strict_mono in IndisputableMonolith.Cryptography.RSCryptographicBound decl_use

depends on (11)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
one_lt_phi in IndisputableMonolith.Constants decl_use
perBitCost in IndisputableMonolith.Cryptography.RSCryptographicBound decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
one_lt_phi in IndisputableMonolith.PhiSupport decl_use
one_lt_phi in IndisputableMonolith.PhiSupport.Lemmas decl_use