theorem proved term proof

`npWorkload_succ`

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

formal statement (Lean)

 104theorem npWorkload_succ (n : ℕ) :
 105    npWorkload (n + 1) = 2 * npWorkload n := by

proof body

Term-mode proof.

 106  unfold npWorkload; rw [pow_succ]; ring
 107
 108/-- **STRUCTURAL DOUBLING.** Each additional input bit forces a doubling
 109of the bandwidth budget required. -/

used by (4)

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

doubling_separation in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
pVsNPFromBITCert in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
PvsNPFromBITCert in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
pvsNP_one_statement in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use

depends on (9)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
npWorkload in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
required in IndisputableMonolith.Foundation.DomainBootstrap decl_use
forces in IndisputableMonolith.Foundation.MagnitudeOfMismatch decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
bandwidth in IndisputableMonolith.Unification.RecognitionBandwidth decl_use